diff options
| author | Enrico Tassi | 2019-02-22 20:52:14 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-02-22 20:52:14 +0100 |
| commit | dea9f08178efcf9cfac7ee2970dc21abc2fde308 (patch) | |
| tree | 515a3caec0fd881b71ac1cdbab743cfb5fd473bf /man | |
| parent | 6a289e4fbc1c4327429bb7041e8f39a18bbb0f70 (diff) | |
| parent | e8419bac30ab98527ec6b15d5a0f5c1035539ca5 (diff) | |
Merge PR #9576: [library] Remove `-boot` option.
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
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 |