diff options
Diffstat (limited to 'contrib/xml/xmlentries.ml4')
| -rw-r--r-- | contrib/xml/xmlentries.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4 index d81269702..876da02e2 100644 --- a/contrib/xml/xmlentries.ml4 +++ b/contrib/xml/xmlentries.ml4 @@ -88,7 +88,7 @@ VERNAC COMMAND EXTEND Xml | [ "Print" "XML" "All" ] -> [ Xmlcommand.printAll () ] | [ "Print" "XML" "Module" diskname(dn) qualid(id) ] -> - [ Xmlcommand.printModule id dn ] + [ Xmlcommand.printLibrary id dn ] | [ "Print" "XML" "Section" diskname(dn) ident(id) ] -> [ Xmlcommand.printSection id dn ] |