diff options
Diffstat (limited to 'doc/RefMan-com.tex')
| -rwxr-xr-x | doc/RefMan-com.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/RefMan-com.tex b/doc/RefMan-com.tex index aaef1943f0..ddb39f2422 100755 --- a/doc/RefMan-com.tex +++ b/doc/RefMan-com.tex @@ -153,13 +153,13 @@ The following command-line options are recognized by the commands {\tt \item[{\tt -compile} {\em file}]\ \\ This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo}. - This option implies option {\tt -batch} and {\tt -silent}. It is + This option implies options {\tt -batch} and {\tt -silent}. It is only available for {\tt coqtop}. %\item[{\tt -compile-verbose} {\em file}]\ \\ % This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo} with % a copy of the contents of the file on standard input. -% This option implies option {\tt -batch} and {\tt -silent}. It is +% This option implies options {\tt -batch} and {\tt -silent}. It is % only available for {\tt coqtop}. \item[{\tt -batch}]\ \\ |