aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/usage.ml
diff options
context:
space:
mode:
authorGravatar courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-19 06:49:50 +0000
committerGravatar courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-19 06:49:50 +0000
commit831886a339af8bd5cd14f9d7e5ea4f9ff9ecd744 (patch)
tree10dfbd93f7d18df58ad25f5194a2ef8527e81fdf /toplevel/usage.ml
parent5c18d2b232c85b8148ec86bd453440a634c38230 (diff)
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1612 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/usage.ml')
-rw-r--r--toplevel/usage.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 8dc848d3c..f9d5decd9 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -47,6 +47,7 @@ let print_usage_channel co command =
-init-file f set the rcfile to f
-user u use the rcfile of user u
-batch batch mode (exits just after arguments parsing)
+ -boot boot mode (implies -q and -batch)
-emacs tells Coq it is executed under Emacs
"