pdf docs: scale down monospace font

2020-05-03 08:23:35 +02:00
parent 15d74eaaf4
commit 26d29e0ec7
2 changed files with 6 additions and 6 deletions
--- a/docs/conf.py
+++ b/docs/conf.py
@ -267,7 +267,7 @@ latex_elements = {
    'fontpkg': r'''
 \setmainfont{DejaVu Serif}
 \setsansfont{DejaVu Sans}
-\setmonofont{DejaVu Sans Mono}
+\setmonofont{DejaVu Sans Mono}[Scale=0.8]
 ''',

     # Additional stuff for the LaTeX preamble.