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
@@ -101,5 +101,5 @@ latex_elements = {
     'inputenc': '',
     'utf8extra': '',
-    'preamble': '''
+    'preamble': r'''
 \usepackage{fontspec}
 \usepackage{makeidx}
@@ -107,5 +107,5 @@ latex_elements = {
 \setromanfont{DejaVu Serif}
 \setmonofont{DejaVu Sans Mono}
-\setlength{\\tymin}{45pt}
+\setlength{\tymin}{45pt}
 ''',
 }