diff options
| author | herbelin | 2002-09-27 23:05:38 +0000 |
|---|---|---|
| committer | herbelin | 2002-09-27 23:05:38 +0000 |
| commit | 310344332e3f995646c5a95d9ff08b025f610cef (patch) | |
| tree | 83aa3322a4d85bb3690287eacbb6be93902aaa30 | |
| parent | cd8b65e09278778c95ea4f8bc03b96ec4d9cafcf (diff) | |
Filtrage redondant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3042 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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; |