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 | |
| 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')
| -rw-r--r-- | man/coqide.1 | 9 | ||||
| -rw-r--r-- | man/coqtop.1 | 6 |
2 files changed, 0 insertions, 15 deletions
diff --git a/man/coqide.1 b/man/coqide.1 index 3592f6e4e3..62a102af03 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -100,15 +100,6 @@ Skip loading of rcfile. Set the rcfile to .IR f . .TP -.B \-batch -Batch mode (exits just after arguments parsing). -.TP -.B \-boot -Boot mode (implies -.B \-q -and -.BR \-batch ). -.TP .B \-emacs Tells Coq it is executed under Emacs. .TP 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 |