diff options
| author | Maxime Dénès | 2016-11-10 13:24:28 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-14 14:17:11 +0100 |
| commit | 30f222b1aad7ec483902b74dfa7dad7aefd5fca3 (patch) | |
| tree | 9a4106bf39d7ec15b07e845324844ea25160ced8 /toplevel | |
| parent | 7e992fa784ee6fa48af8a2e461385c094985587d (diff) | |
Do not mention "none" in warnings doc, as it is there for compatibility.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/usage.ml | 4 |
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\ |