diff options
| -rw-r--r-- | docs/users_guide/conf.py | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/docs/users_guide/conf.py b/docs/users_guide/conf.py index 597d6765c7..802d4c7e92 100644 --- a/docs/users_guide/conf.py +++ b/docs/users_guide/conf.py @@ -107,6 +107,10 @@ latex_elements = { \setromanfont{DejaVu Serif} \setmonofont{DejaVu Sans Mono} \setlength{\\tymin}{45pt} + +% Avoid a torrent of over-full \hbox warnings +\usepackage{microtype} +\hbadness=99999 ''', } |