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
---
 toplevel/usage.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'toplevel/usage.ml')

diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 124ce0593e..417a496f8a 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -57,7 +57,8 @@ let print_usage_channel co command =
   -batch                 batch mode (exits just after arguments parsing)
   -boot                  boot mode (implies -q and -batch)
   -emacs                 tells Coq it is executed under Emacs
-  -no-glob f             do not dump globalizations
+  -noglob f              do not dump globalizations
+  -dump-glob f           dump globalizations in file f (to be used by coqdoc)
   -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)
   -impredicative-set     set sort Set impredicative
   -dont-load-proofs      don't load opaque proofs in memory
-- 
cgit v1.2.3