diff --git a/srcpkgs/ghc/patches/sphinx-unicode.patch b/srcpkgs/ghc/patches/sphinx-unicode.patch new file mode 100644 index 00000000000..0286b9c2bd3 --- /dev/null +++ b/srcpkgs/ghc/patches/sphinx-unicode.patch @@ -0,0 +1,17 @@ +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} + ''', + }