From fe487e8eaae3186803ec657c517d0ebebab3bafd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 8 May 2019 22:42:48 +0200
Subject: An even more uniform treatment of the -help option across
 executables.

Incidentally fix some missing newline in coqc help, and give proper
help for coqidetop and the "coq*worker"s.
---
 ide/idetop.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'ide')

diff --git a/ide/idetop.ml b/ide/idetop.ml
index f79ad5deab..eb76951b44 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -552,8 +552,10 @@ let rec parse = function
        x :: parse rest
   | [] -> []
 
-let () = Usage.add_to_usage "coqidetop"
-"  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format\
+let () = Usage.add_to_usage "coqidetop" "" "\n\
+coqidetop specific options:\n\
+\n  --xml_formatinclude dir           (idem)\
+\n  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format\
 \n  --help-XML-protocol    print documentation of the Coq XML protocol\n"
 
 let islave_parse ~opts extra_args =
@@ -580,7 +582,7 @@ let () =
   let open Coqtop in
   let custom = {
       parse_extra = islave_parse ;
-      help = (fun _ -> output_string stderr "Same options as coqtop");
+      help = Usage.print_usage "coqidetop";
       init = islave_init;
       run = loop;
       opts = islave_default_opts } in
-- 
cgit v1.2.3