841d9c7fc1
GitOrigin-RevId: 3a8d7958a610cd3fec3a6f424480f91a1b259185
11 lines
355 B
Diff
11 lines
355 B
Diff
--- ghc-8.10.4/docs/users_guide/conf.py.orig 2021-06-21 13:46:34.196383559 +0200
|
|
+++ ghc-8.10.4/docs/users_guide/conf.py 2021-06-21 13:46:54.839349941 +0200
|
|
@@ -100,7 +100,7 @@
|
|
latex_elements = {
|
|
'inputenc': '',
|
|
'utf8extra': '',
|
|
- 'preamble': '''
|
|
+ 'preamble': r'''
|
|
\usepackage{fontspec}
|
|
\usepackage{makeidx}
|
|
\setsansfont{DejaVu Sans}
|