clean_string: map "_" to "\\_" (best used with underscore.sty);
authorwenzelm
Thu May 08 22:17:37 2008 +0200 (2008-05-08)
changeset 2685352cb0e965041
parent 26852 a31203f58b20
child 26854 9b4aec46ad78
clean_string: map "_" to "\\_" (best used with underscore.sty);
doc-src/antiquote_setup.ML
     1.1 --- a/doc-src/antiquote_setup.ML	Thu May 08 22:05:15 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Thu May 08 22:17:37 2008 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  (* misc utils *)
     1.5  
     1.6  val clean_string = translate_string
     1.7 -  (fn "_" => "-"
     1.8 +  (fn "_" => "\\_"
     1.9      | ">" => "$>$"
    1.10      | "#" => "\\#"
    1.11      | "{" => "\\{"