diff options
Diffstat (limited to 'doc/refman/RefMan-com.tex')
| -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 892c9931b..8b1fc7c8f 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -214,11 +214,6 @@ The following command-line options are recognized by the commands {\tt % % Switch on the debug flag. -\item[{\tt -with-geoproof} (yes|no)]\ % - - Enable or not special functions for Geoproof within {\CoqIDE} (default - is yes). - \item[{\tt -color} (on|off|auto)]\ % Enable or not the coloring of output of {\tt coqtop}. Default is auto, |