aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b97042ede..f3bcee128 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -298,6 +298,7 @@ let parse_args arglist =
|"-filteropts" -> filter_opts := true
|"-force-load-proofs" -> Flags.load_proofs := Flags.Force
|"-h"|"-H"|"-?"|"-help"|"--help" -> usage ()
+ |"--help-XML-protocol" -> Serialize.document Xml_printer.to_string_fmt; exit 0
|"-ideslave" -> Flags.ide_slave := true
|"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet
|"-just-parsing" -> Vernac.just_parsing := true