# HG changeset patch
# User wenzelm
# Date 1210277857 -7200
# Node ID 52cb0e9650411647b7d6f6ad31758ff6a1996078
# Parent  a31203f58b206bf820cd0d1b4c9349ca15cec703
clean_string: map "_" to "\\_" (best used with underscore.sty);

diff -r a31203f58b20 -r 52cb0e965041 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Thu May 08 22:05:15 2008 +0200
+++ b/doc-src/antiquote_setup.ML	Thu May 08 22:17:37 2008 +0200
@@ -14,7 +14,7 @@
 (* misc utils *)
 
 val clean_string = translate_string
-  (fn "_" => "-"
+  (fn "_" => "\\_"
     | ">" => "$>$"
     | "#" => "\\#"
     | "{" => "\\{"