From e46a0b49164e5e4f406a22ef66de02dd6a96c3b1 Mon Sep 17 00:00:00 2001
From: notin
Date: Tue, 9 Sep 2008 09:33:44 +0000
Subject: Suppression d'un warning inutile

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11392 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 scripts/coqc.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'scripts')

diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 0fb704f7ac..e661455cac 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -136,7 +136,6 @@ let parse_args () =
     | ("-db"|"-debugger") :: rem ->
         print_string "Warning: option -db/-debugger deprecated\n";flush stdout;
         parse (cfiles,args) rem
-    | "-dump-glob" :: _ :: rem -> Pp.msg_warning (Pp.str "option -dumpglob is obsolete"); parse (cfiles,args) rem
 
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
     | ("-I"|"-include"|"-outputstate"
-- 
cgit v1.2.3