clean_name: replace "_" by "-";
authorwenzelm
Thu, 15 May 2008 18:03:47 +0200
changeset 26903 0542898ab667
parent 26902 8db1e960d636
child 26904 e90832d7196a
clean_name: replace "_" by "-";
doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Thu May 15 17:39:20 2008 +0200
+++ b/doc-src/antiquote_setup.ML	Thu May 15 18:03:47 2008 +0200
@@ -27,7 +27,7 @@
   | clean_name "." = "dot"
   | clean_name "{" = "braceleft"
   | clean_name "}" = "braceright"
-  | clean_name s = s;
+  | clean_name s = s |> translate_string (fn "_" => "-" | c => c);
 
 val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;