diff options
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index bcee6d0ce6..c9fa6a18c2 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -195,6 +195,8 @@ let parse_args () = | ("-m" | "--memory") :: rem -> memory_stat := true; parse rem + | "-xml" :: rem -> Options.xml_export := true; parse rem + | s :: _ -> prerr_endline ("Don't know what to do with " ^ s); usage () in |