@@ -0,0 +1,20 @@
1+diff --git a/docs/users_guide/conf.py b/docs/users_guide/conf.py
2+index 0732c5ccd4..47db25b84a 100644
3+--- a/docs/users_guide/conf.py
4++++ b/docs/users_guide/conf.py
5+@@ -77,13 +77,13 @@ htmlhelp_basename = 'GHCUsersGuide'
11+ \usepackage{fontspec}
13+ \setsansfont{DejaVu Sans}
14+ \setromanfont{DejaVu Serif}
15+ \setmonofont{DejaVu Sans Mono}
16+-\setlength{\\tymin}{45pt}
17++\setlength{\tymin}{45pt}