author | wenzelm |
Thu, 15 May 2008 18:03:47 +0200 | |
changeset 26903 | 0542898ab667 |
parent 26902 | 8db1e960d636 |
child 26904 | e90832d7196a |
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