diff options
Diffstat (limited to 'coq/coq-par-compile.el')
| -rw-r--r-- | coq/coq-par-compile.el | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index 109b2c2d..a04892b7 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -21,7 +21,6 @@ ;; - on error, try to location info into the error message ;; - handle missing coqdep/coqc gracefully ;; - 'all-cores option for coq-max-background-compilation-jobs -;; - write user manual ;; (eval-when-compile @@ -685,7 +684,7 @@ case, the following actions are taken: (get job 'name)))) (if coq-debug-auto-compilation (message "%s: has itself no queue dependency" (get job 'name))) - (when (get job 'require-span) + (when (and (get job 'require-span) coq-lock-ancestors) (let ((span (get job 'require-span))) (dolist (f (get job 'ancestor-files)) (unless (eq (gethash f coq-par-ancestor-files) 'asserted) @@ -821,10 +820,11 @@ Besides starting the background process, the source file is locked, registered in the 'ancestor-files property of JOB and in `coq-par-ancestor-files'" (let ((true-src (file-truename (get job 'src-file)))) - (proof-register-possibly-new-processed-file true-src) - (put job 'ancestor-files (list true-src)) - (unless (gethash true-src coq-par-ancestor-files) - (puthash true-src 'locked coq-par-ancestor-files)) + (when coq-lock-ancestors + (proof-register-possibly-new-processed-file true-src) + (put job 'ancestor-files (list true-src)) + (unless (gethash true-src coq-par-ancestor-files) + (puthash true-src 'locked coq-par-ancestor-files))) (coq-par-start-process coq-dependency-analyzer (coq-par-coq-arguments (get job 'src-file) (get job 'load-path)) |