aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorEnrico Tassi2018-08-21 11:12:18 +0200
committerEnrico Tassi2018-08-21 11:12:18 +0200
commit5a9aaa0423fff6be693a28c0ced0f8dbcbe79551 (patch)
tree837a29579e8e4adb79bdbc8c8a7e0d7fbc631fad /tools
parent449c9384f93c5af82d58baf280c7c17accee86d2 (diff)
[coq_makefile] print all options (Fix #7529)
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_makefile.ml34
1 files changed, 13 insertions, 21 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index ad489da822..c3bdf656d1 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -31,8 +31,19 @@ let rec print_prefix_list sep = function
| x :: l -> print sep; print x; print_prefix_list sep l
| [] -> ()
-let usage_common () =
+let usage_coq_makefile () =
+ output_string stderr "Usage summary:\
+\n\
+\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\
+\n ... [any] ... [-extra[-phony] result dependencies command]\
+\n ... [-I dir] ... [-R physicalpath logicalpath]\
+\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\
+\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\
+\n [-h] [--help]\
+\n";
output_string stderr "\
+\nFull list of options:\
+\n\
\n[file.v]: Coq file to be compiled\
\n[file.ml[i4]?]: Objective Caml file to be compiled\
\n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\
@@ -61,25 +72,6 @@ let usage_common () =
\n[-install opt]: where opt is \"user\" to force install into user directory,\
\n \"none\" to build a makefile with no install target or\
\n \"global\" to force install in $COQLIB directory\
-\n"
-
-let usage_coq_project () =
- output_string stderr "Available arguments:";
- usage_common ();
- exit 1
-
-let usage_coq_makefile () =
- output_string stderr "Usage summary:\
-\n\
-\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\
-\n ... [any] ... [-extra[-phony] result dependencies command]\
-\n ... [-I dir] ... [-R physicalpath logicalpath]\
-\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\
-\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\
-\n [-h] [--help]\
-\n";
- usage_common ();
- output_string stderr "\
\n[-f file]: take the contents of file as arguments\
\n[-o file]: output should go in file file (recommended)\
\n Output file outside the current directory is forbidden.\
@@ -405,7 +397,7 @@ let _ =
let project =
try cmdline_args_to_project ~curdir:Filename.current_dir_name args
- with Parsing_error s -> prerr_endline s; usage_coq_project () in
+ with Parsing_error s -> prerr_endline s; usage_coq_makefile () in
if only_destination <> None then begin
destination_of project (Option.get only_destination);