From d6f4f3f3dc92d805bc046bcdbc30dd7df65fb4aa Mon Sep 17 00:00:00 2001
From: notin
Date: Fri, 18 Jul 2008 15:58:12 +0000
Subject: Rétablissement de l'option -dump-glob de coq top et de l'option
 -glob-from de coqdoc (compatibilité)

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

(limited to 'scripts')

diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 84f12049ad..6915d60bc9 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" as o) :: rem ->
+      |"-init-file" | "-dump-glob" as o) :: rem ->
 	begin
 	  match rem with
 	    | s :: rem' -> parse (cfiles,s::o::args) rem'
-- 
cgit v1.2.3