aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-abbrev.el
diff options
context:
space:
mode:
authorGravatar Hendrik Tews <hendrik@askra.de>2016-12-08 16:06:17 +0100
committerGravatar Hendrik Tews <hendrik@askra.de>2016-12-08 16:06:17 +0100
commit687e008bc80ca6f66ca8920296c2e8dab889c752 (patch)
tree970bed3af3a948a02eb19502c45763eb75e984c5 /coq/coq-abbrev.el
parentcde8f9e4a13ec2d05c8435be16da02e54e6b5a70 (diff)
option coq-compile-keep-going for parallel compilation
With this option set, compilation continues after the first error to compile as much as possible and to potentially report more than one error.
Diffstat (limited to 'coq/coq-abbrev.el')
-rw-r--r--coq/coq-abbrev.el10
1 files changed, 9 insertions, 1 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 767d2a6e..ec8d5e80 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -161,7 +161,15 @@ It was constructed with `proof-defstringset-fn'.")
:active coq-compile-before-require
:help ,(concat "Compile parallel in background or "
"sequentially with blocking ProofGeneral.")]
- ["no quick"
+ ["Keep going"
+ coq-compile-keep-going-toggle
+ :style toggle
+ :selected coq-compile-keep-going
+ :active (and coq-compile-before-require
+ coq-compile-parallel-in-background)
+ :help ,(concat "Continue background compilation after "
+ "the first error as far as possible")]
+ ["no quick"
(customize-set-variable 'coq-compile-quick 'no-quick)
:style radio
:selected (eq coq-compile-quick 'no-quick)