From 346df3d1336bfa01bc6e58ea08245b67d3127a00 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 15 Nov 2014 21:28:25 +0100
Subject: For consistency with other coqtop flags, use -help rather than --help
 in usage.

---
 toplevel/coqtop.ml | 4 ++--
 toplevel/usage.ml  | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 4fa3450830..4580e49b1c 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -278,7 +278,7 @@ let print_style_tags () =
 
 let error_missing_arg s =
   prerr_endline ("Error: extra argument expected after option "^s);
-  prerr_endline "See --help for the syntax of supported options";
+  prerr_endline "See -help for the syntax of supported options";
   exit 1
 
 let filter_opts = ref false
@@ -554,7 +554,7 @@ let init arglist =
       let extras = !toploop_init extras in
       if not (List.is_empty extras) then begin
         prerr_endline ("Don't know what to do with "^String.concat " " extras);
-        prerr_endline "See --help for the list of supported options";
+        prerr_endline "See -help for the list of supported options";
         exit 1
       end;
       if_verbose print_header ();
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 1efccefbac..a85f2f5c26 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -67,7 +67,7 @@ let print_usage_channel co command =
 \n  -impredicative-set     set sort Set impredicative\
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -time                  display the time taken by each command\
-\n  -h, --help             print this list of options\
+\n  -h, -help              print this list of options\
 \n";
   List.iter (fun (name, text) ->
     output_string co
-- 
cgit v1.2.3