diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-com.tex | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 076519dc61..0f4bb342ab 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -178,11 +178,6 @@ The following command-line options are recognized by the commands {\tt Cause \Coq~not to load the resource file. -\item[{\tt -user} {\em username}]\ - - Take resource file of user {\em username} (that is - \verb+~+{\em username}{\tt /.coqrc.7.0}) instead of yours. - \item[{\tt -load-ml-source} {\em file}]\ Load the Caml source file {\em file}. |