--- 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}