src/Doc/Sledgehammer/document/root.tex
changeset 55290 3951ced4156c
parent 55289 30d874dc7000
child 55297 1dfcd49f5dcb
--- a/src/Doc/Sledgehammer/document/root.tex	Mon Feb 03 17:18:38 2014 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Mon Feb 03 17:55:50 2014 +0100
@@ -42,6 +42,8 @@
 
 \urlstyle{tt}
 
+\renewcommand\_{\hbox{\textunderscore\kern-.05ex}}
+
 \begin{document}
 
 %%% TYPESETTING