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 | |
| parent | 7e992fa784ee6fa48af8a2e461385c094985587d (diff) | |
Do not mention "none" in warnings doc, as it is there for compatibility.
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 22 | ||||
| -rw-r--r-- | toplevel/usage.ml | 4 |
2 files changed, 13 insertions, 13 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 3a9db5ead2..56ce753cd6 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -914,18 +914,18 @@ This command turns off the normal displaying. \subsection[\tt Unset Silent.]{\tt Unset Silent.\optindex{Silent}} This command turns the normal display on. -\subsection[\tt Set Warnings (\nterm{all}|\nterm{none}|\nterm{w}$_1$,\ldots,% - \nterm{w}$_n$).]{{\tt Set Warnings (\nterm{all}|\nterm{none}|\nterm{w}$_1$,\ldots,% - \nterm{w}$_n$)}.\optindex{Warnings}} +\subsection[\tt Set Warnings ``(\nterm{w}$_1$,\ldots,% + \nterm{w}$_n$)''.]{{\tt Set Warnings ``(\nterm{w}$_1$,\ldots,% + \nterm{w}$_n$)''}.\optindex{Warnings}} \label{SetWarnings} -This command configures the display of warnings. It is experimental, and expects -\texttt{all}, \texttt{none} or a comma-separated list of warning names or -categories. Adding~\texttt{-} in front of a warning disables it, -adding~\texttt{+} makes it an error. It is possible to use the special categories -\texttt{all} and \texttt{default}, the latter containing the warnings enabled by -default. The flags are interpreted from left to right, so in case of an overlap, -the flags on the right have higher priority, meaning that \texttt{A,-A} is -equivalent to \texttt{-A}. +This command configures the display of warnings. It is experimental, and +expects, between quotes, a comma-separated list of warning names or +categories. Adding~\texttt{-} in front of a warning or category disables it, +adding~\texttt{+} makes it an error. It is possible to use the special +categories \texttt{all} and \texttt{default}, the latter containing the warnings +enabled by default. The flags are interpreted from left to right, so in case of +an overlap, the flags on the right have higher priority, meaning that +\texttt{A,-A} is equivalent to \texttt{-A}. \subsection[\tt Set Search Output Name Only.]{\tt Set Search Output Name Only.\optindex{Search Output Name Only} \label{Search-Output-Name-Only} 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\ |