aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/usage.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/usage.ml')
-rw-r--r--toplevel/usage.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index de41f7b19..956a40261 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) 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\