diff options
Diffstat (limited to 'parsing/g_xml.ml4')
| -rw-r--r-- | parsing/g_xml.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index e1a43c400..53ade7c2c 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -79,7 +79,7 @@ let get_xml_attr s al = (* Interpreting specific attributes *) -let ident_of_cdata (loc,a) = id_of_string a +let ident_of_cdata (loc,a) = Id.of_string a let uri_of_data s = let n = String.index s ':' in |