diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 891d41e6cf..d9b7aaa8df 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -346,7 +346,7 @@ let rec process_cmd_line = function Include d :: (process_cmd_line r) | "-R" :: p :: l :: r -> RInclude (p,l) :: (process_cmd_line r) - | ("-I" | "-h" | "--help" | "-custom") :: _ -> + | ("-I"|"-custom") :: _ -> usage () | "-f" :: file :: r -> make_name := file; |