diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-04 19:46:50 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-12-23 02:35:25 +0100 |
| commit | 143244e0606a790b73da2360fb0eabe3d98d4b4e (patch) | |
| tree | e9bccdb8961ce6444f64fab557397e2a8e3ed093 /tools/coq_makefile.ml | |
| parent | d9f79d97dbc503e149cba2df1b228a94d7ac970b (diff) | |
Removing failure of coq_makefile on no arguments.
Nevertheless making option -o of coq_makefile recommended as discussed
in PR#6040.
This is one way to resolve the inconsistency with the usage which says
that all arguments are optional.
Diffstat (limited to 'tools/coq_makefile.ml')
| -rw-r--r-- | tools/coq_makefile.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 2feaaa04c..28fca0a82 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -66,7 +66,7 @@ let usage () = \n \"none\" to build a makefile with no install target or\ \n \"global\" to force install in $COQLIB directory\ \n[-f file]: take the contents of file as arguments\ -\n[-o file]: output should go in file file\ +\n[-o file]: output should go in file file (recommended)\ \n Output file outside the current directory is forbidden.\ \n[-bypass-API]: when compiling plugins, bypass Coq API\ \n[-h]: print this usage summary\ @@ -381,7 +381,6 @@ let share_prefix s1 s2 = let _ = let prog, args = - if Array.length Sys.argv = 1 then usage (); let args = Array.to_list Sys.argv in let prog = List.hd args in prog, List.tl args in |