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