diff options
| author | Emilio Jesus Gallego Arias | 2019-02-12 02:41:00 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-22 14:39:31 +0100 |
| commit | e8419bac30ab98527ec6b15d5a0f5c1035539ca5 (patch) | |
| tree | a9e2766e23ccb0afac63edac44f4442a92686501 /man/coqtop.1 | |
| parent | fa3a97426013cf940cd25abde43c0191766218b1 (diff) | |
[library] Remove `-boot` option.
The `-boot` option was used to:
- suppress loading of the rc_file
- allow to save modules with prefix `Coq`
There is no good reason disable saving of modules with `Coq` prefix by
default, thus we remove this option.
Fixes: #9575
Diffstat (limited to 'man/coqtop.1')
| -rw-r--r-- | man/coqtop.1 | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/man/coqtop.1 b/man/coqtop.1 index addfb54672..25d0ef7718 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -106,12 +106,6 @@ set the rcfile to batch mode (exits just after arguments parsing) .TP -.B \-boot -boot mode (implies -.B \-q -) - -.TP .B \-emacs tells Coq it is executed under Emacs |