diff options
| author | Enrico Tassi | 2018-08-21 11:12:18 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-08-21 11:12:18 +0200 |
| commit | 5a9aaa0423fff6be693a28c0ced0f8dbcbe79551 (patch) | |
| tree | 837a29579e8e4adb79bdbc8c8a7e0d7fbc631fad /tools | |
| parent | 449c9384f93c5af82d58baf280c7c17accee86d2 (diff) | |
[coq_makefile] print all options (Fix #7529)
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 34 |
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); |
