aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/ex
diff options
context:
space:
mode:
authorGravatar Hendrik Tews <hendrik@askra.de>2012-11-13 22:05:11 +0000
committerGravatar Hendrik Tews <hendrik@askra.de>2012-11-13 22:05:11 +0000
commit2243cc9d87d4993ca6b0281f7171b883dd9fd52d (patch)
tree10b5d50bc8003df6a6d7f90973ecd60f779649c7 /coq/ex
parent06b2407614a9f81795e47d2710826d0973edbaf1 (diff)
- first version of parallel asynchronous compilation for coq in
coq-par-compile.el (must be activated via coq-compile-parallel-in-background) - items in the queue region are not necessarily in proof-action-list any more! Require commands and the following items are stored elsewhere until the compilation finishes. Variable proof-second-action-list-active notifies the generic machinery if queue items are stored elsewhere. In this case, Proof General must neither release the proof shell lock nor delete the queue span when proof-action-list is empty. - to kill background processes as early as possible, the new hook proof-shell-signal-interrupt-hook is used
Diffstat (limited to 'coq/ex')
-rw-r--r--coq/ex/test-cases/README1
1 files changed, 0 insertions, 1 deletions
diff --git a/coq/ex/test-cases/README b/coq/ex/test-cases/README
index d719e333..00917b7f 100644
--- a/coq/ex/test-cases/README
+++ b/coq/ex/test-cases/README
@@ -12,7 +12,6 @@ add-load-path-unsupported
change-ancestor
assert something just added to an completely locked ancestor
- (triggers known bugs)
multiple-files-multiple-dir
working with multiple files in multiple directories