diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-09-28 16:56:22 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2016-11-04 11:15:25 +0100 |
| commit | 5939d426ac785ec063e66a302f3692b645993c56 (patch) | |
| tree | 499db9b859620ffcf0fe6bded9cf3dbc572ad382 /toplevel | |
| parent | 962a5d3526290b83967a92ef1eb772894d10362b (diff) | |
Add documentation for [Set Warnings] and the -w option.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/usage.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index de41f7b19..2bde1dc46 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -62,7 +62,7 @@ let print_usage_channel co command = \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 -w (all|none|w1,..,wn) configure display of warnings\ \n -color (yes|no|auto) configure color output\ \n\ \n -q skip loading of rcfile\ |