diff options
| author | Hendrik Tews | 2020-10-31 13:10:28 +0100 |
|---|---|---|
| committer | hendriktews | 2020-12-19 16:43:49 +0100 |
| commit | e90af80638d5e367f5e7f9d8e0af5dd9028e2377 (patch) | |
| tree | a22724d18e9ee1aa25357fc5f11c8b4a5ca217f3 /coq/coq-compile-common.el | |
| parent | 9064f143b7aae41cfcbfcf5270ab69a81887f21f (diff) | |
redesign of parallel background compilation without clones
- no clones any more, existing jobs are directly linked
- the whole require command is processed by coqdep to determine
the required files, this fixes #352
- the require commands are a separate kind of jobs, because they
do not need to get compiled
- queue items are only stored in require jobs and file jobs can
not have a queue dependency, this simplifies the logic
Diffstat (limited to 'coq/coq-compile-common.el')
| -rw-r--r-- | coq/coq-compile-common.el | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 938f706e..ed927409 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -626,6 +626,7 @@ Changes the suffix from .vo to .vok. VO-OBJ-FILE must have a .vo suffix." ;;; manage coq--compile-response-buffer +;; XXX apparently nobody calls this with display equal to nil (defun coq-compile-display-error (command error-message display) "Display COMMAND and ERROR-MESSAGE in `coq--compile-response-buffer'. If needed, reinitialize `coq--compile-response-buffer'. Then |