aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/usage.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 2bde1dc46b..956a402617 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -61,8 +61,8 @@ let print_usage_channel co command =
\n -v print Coq version and exit\
\n -list-tags print highlight color tags known by Coq and exit\
\n\
-\n -quiet unset display of extra information (implies -w none)\
-\n -w (all|none|w1,..,wn) configure display of warnings\
+\n -quiet unset display of extra information (implies -w \"-all\")\
+\n -w (w1,..,wn) configure display of warnings\
\n -color (yes|no|auto) configure color output\
\n\
\n -q skip loading of rcfile\