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 84e4a5732..992f9c59a 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -58,7 +58,7 @@ END let error_bad_arity loc n = let s = match n with 0 -> "none" | 1 -> "one" | 2 -> "two" | _ -> "many" in - user_err_loc (loc,"",str ("wrong number of arguments (expect "^s^").")) + user_err_loc (loc,"",str "wrong number of arguments (expect " ++ str s ++ str ").") (* Interpreting attributes *) |