# HG changeset patch
# User wenzelm
# Date 1210874560 -7200
# Node ID aa6357b39212b1b0341314a51ac94f7ef0e494bf
# Parent  f42d638c5f0738c83c7d36ae633919568ad14a09
tuned clean_name (underscore);

diff -r f42d638c5f07 -r aa6357b39212 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Thu May 15 20:02:39 2008 +0200
+++ b/doc-src/antiquote_setup.ML	Thu May 15 20:02:40 2008 +0200
@@ -25,6 +25,7 @@
 fun clean_name "\\<dots>" = "dots"
   | clean_name ".." = "ddot"
   | clean_name "." = "dot"
+  | clean_name "_" = "underscore"
   | clean_name "{" = "braceleft"
   | clean_name "}" = "braceright"
   | clean_name s = s |> translate_string (fn "_" => "-" | c => c);