diff options
Diffstat (limited to 'doc/refman/RefMan-com.tex')
| -rw-r--r-- | doc/refman/RefMan-com.tex | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 6f8584988..c1e552a5d 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -199,6 +199,12 @@ The following command-line options are recognized by the commands {\tt available for {\tt coqc} only; it is the counterpart of {\tt -compile-verbose}. + \item[{\tt -w} (all|none|w$_1$,\ldots,w$_n$)]\ % + + Configure the display of warnings. This option expects {\tt all}, {\tt none} + or a comma-separated list of warning names or categories (see + Section~\ref{SetWarnings}). + %Mostly unused in the code %\item[{\tt -debug}]\ % % |