diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2016-12-08 23:40:51 +0100 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2016-12-08 23:40:51 +0100 |
| commit | cab89d031162b5d964bbc299fe0f451cf0daef71 (patch) | |
| tree | 5b1829eba763fd2da8c4fb1857690032dd3131b6 /coq/coq-compile-common.el | |
| parent | 687e008bc80ca6f66ca8920296c2e8dab889c752 (diff) | |
documentation and CHANGES for coq-compile-keep-going
Diffstat (limited to 'coq/coq-compile-common.el')
| -rw-r--r-- | coq/coq-compile-common.el | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 40e3a4d7..92614e7a 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -234,6 +234,9 @@ quick-and-vio2vo Same as `quick-no-vio2vo', but start vio2vo processes compilation while you are processing stuff far below the last require. vio2vo compilation is done on a subset of the available cores, see `coq-compile-vio2vo-percentage'. + When `coq-compile-keep-going' is set, vio2vo compilation + is scheduled for those files for which coqc compilation + was successful. Warning: This mode does only work when you process require commands in batches. Slowly single-stepping through require's @@ -265,8 +268,11 @@ ensure-vo Ensure that all library dependencies are present as .vo "Continue compilation after the first error as far as possible. Similar to ``make -k'', with this option enabled, the background compilation continues after the first error as far as possible. -With this option disabled, the background compilation is -immediately stopped after the first error.") +With this option disabled, background compilation is +immediately stopped after the first error. + +This option can be set/reset via menu +`Coq -> Auto Compilation -> Keep going'.") ;; define coq-compile-keep-going-toggle (proof-deftoggle coq-compile-keep-going) |