From 310344332e3f995646c5a95d9ff08b025f610cef Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 27 Sep 2002 23:05:38 +0000
Subject: Filtrage redondant

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3042 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tools/coq_makefile.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

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;
-- 
cgit v1.2.3