diff options
Diffstat (limited to 'contrib/xml/xmlentries.ml')
| -rw-r--r-- | contrib/xml/xmlentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/xml/xmlentries.ml b/contrib/xml/xmlentries.ml index 093727f2f1..2323adaa0d 100644 --- a/contrib/xml/xmlentries.ml +++ b/contrib/xml/xmlentries.ml @@ -45,8 +45,8 @@ vinterp_add "XmlPrintAll" vinterp_add "XmlPrintModule" (function - [VARG_IDENTIFIER id] -> (fun () -> Xmlcommand.printModule id None) - | [VARG_IDENTIFIER id ; VARG_STRING dn] -> + [VARG_QUALID id] -> (fun () -> Xmlcommand.printModule id None) + | [VARG_QUALID id ; VARG_STRING dn] -> (fun () -> Xmlcommand.printModule id (Some dn)) | _ -> anomaly "This should be trapped");; |