| changeset 26903 | 0542898ab667 |
| parent 26897 | 044619358d3a |
| child 26910 | aa6357b39212 |
--- 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;