aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqtop.ml1
-rw-r--r--toplevel/usage.ml1
2 files changed, 2 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
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index e9e576962..b8e94c9cc 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -74,6 +74,7 @@ let print_usage_channel co command =
\n some tactics\
\n -time display the time taken by each command\
\n -h, --help print this list of options\
+\n --help-XML-protocol print the documentation of the XML protocol used by CoqIDE\
\n"
(* print the usage on standard error *)