ghc/ghc-userguide-sphinx4.patch

12 lines
347 B
Diff

--- ghc-8.8.4/docs/users_guide/conf.py~ 2020-07-09 00:43:03.000000000 +0800
+++ ghc-8.8.4/docs/users_guide/conf.py 2021-07-01 00:09:03.537324304 +0800
@@ -77,7 +77,7 @@
latex_elements = {
'inputenc': '',
'utf8extra': '',
- 'preamble': '''
+ 'preamble': r'''
\usepackage{fontspec}
\usepackage{makeidx}
\setsansfont{DejaVu Sans}