aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-compile-common.el
diff options
context:
space:
mode:
authorGravatar Hendrik Tews <hendrik@askra.de>2016-11-24 19:45:11 +0100
committerGravatar Hendrik Tews <hendrik@askra.de>2016-11-29 23:49:20 +0100
commitfb178a6313132024c13f27865f97e090466058e3 (patch)
tree98af344b3d67e97e1a9448510f2f041577ae9d1a /coq/coq-compile-common.el
parentf158ae23977cfb40a4a2f7a0db123940f59768f8 (diff)
delay vio2vo compilation
... to make it less likely people run into the library inconsistency issue with vio2vo
Diffstat (limited to 'coq/coq-compile-common.el')
-rw-r--r--coq/coq-compile-common.el8
1 files changed, 8 insertions, 0 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 3522a8f0..57581af3 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -275,6 +275,14 @@ percentage of `coq-max-background-compilation-jobs'."
:set 'coq-max-vio2vo-setter
:group 'coq-auto-compile)
+(defcustom coq-compile-vio2vo-delay 2.5
+ "Delay in seconds for the vio2vo compilation.
+This delay helps to avoid running into a library inconsistency
+with 'quick-and-vio2vo, see Coq issue #5223."
+ :type 'number
+ :safe 'numberp
+ :group 'coq-auto-compile)
+
(defcustom coq-compile-command ""
"External compilation command. If empty ProofGeneral compiles itself.
If unset (the empty string) ProofGeneral computes the dependencies of