From 4823449f7f3800835bfd5ebc4de5bdf407fdc2c2 Mon Sep 17 00:00:00 2001
From: notin
Date: Tue, 24 Jun 2008 11:41:12 +0000
Subject: Suppression de l'option -dump-glob et ajout d'une option -no-glob

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

(limited to 'scripts')

diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 673567a856..84f12049ad 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -141,7 +141,7 @@ let parse_args () =
     | ("-I"|"-include"|"-outputstate"
       |"-inputstate"|"-is"|"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"|"-user"
-      |"-init-file"|"-dump-glob" as o) :: rem ->
+      |"-init-file" as o) :: rem ->
 	begin
 	  match rem with
 	    | s :: rem' -> parse (cfiles,s::o::args) rem'
@@ -151,13 +151,16 @@ let parse_args () =
 
     | ("-notactics"|"-debug"|"-nolib"
       | "-debugVM"|"-alltransp"|"-VMno"
-      |"-batch"|"-nois"
+      |"-batch"|"-nois" | "-noglob" | "-no-glob"
       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
       |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-translate" |"-strict-implicit"
       |"-dont-load-proofs"|"-impredicative-set"|"-vm" 
       | "-unboxed-values" | "-unboxed-definitions" | "-draw-vm-instr" 
 	  as o) :: rem ->
 	parse (cfiles,o::args) rem
+
+    | "-dump-glob" :: _ :: rem -> Pp.msg_warning (Pp.str "option -dumpglob is obsolete"); parse (cfiles,args) rem
+
     | "-where" :: _ -> 
 	let coqlib = 
 	  try Sys.getenv "COQLIB" with Not_found -> Coq_config.coqlib 
-- 
cgit v1.2.3