18 lines
569 B
Diff
18 lines
569 B
Diff
|
diff -rpU2 ghc-8.8.4-orig/docs/users_guide/conf.py ghc-8.8.4/docs/users_guide/conf.py
|
||
|
|
--- ghc-8.8.4-orig/docs/users_guide/conf.py 2020-07-08 16:43:03.000000000 +0000
|
||
|
|
+++ ghc-8.8.4/docs/users_guide/conf.py 2021-07-10 20:25:33.536928487 +0000
|
||
|
|
@@ -78,5 +78,5 @@ latex_elements = {
|
||
|
|
'inputenc': '',
|
||
|
|
'utf8extra': '',
|
||
|
|
- 'preamble': '''
|
||
|
|
+ 'preamble': r'''
|
||
|
|
\usepackage{fontspec}
|
||
|
|
\usepackage{makeidx}
|
||
|
|
@@ -84,5 +84,5 @@ latex_elements = {
|
||
|
|
\setromanfont{DejaVu Serif}
|
||
|
|
\setmonofont{DejaVu Sans Mono}
|
||
|
|
-\setlength{\\tymin}{45pt}
|
||
|
|
+\setlength{\tymin}{45pt}
|
||
|
|
''',
|
||
|
|
}
|