diff options
| author | Hendrik Tews | 2019-08-20 23:02:33 +0200 |
|---|---|---|
| committer | Hendrik Tews | 2019-08-21 08:38:33 +0200 |
| commit | 4f46b3ff3c904663c99457fbe1ed1a63a5e739b2 (patch) | |
| tree | 08a582677df7611dfdb2618666da36f11b4d40be | |
| parent | aa36785c6e7166da0720e05ba708cdf22687a9d9 (diff) | |
coq-par-compile: fix 8.10 -schedule-vio2vo incompatibility
Use coqc for vio2vo compilation instead of coqtop for
Coq >= 8.10+alpha.
With https://github.com/coq/coq/pull/8690 vio2vo
compilation (-schedule-vio2vo) was moved from coqtop to coqc, see
also https://github.com/coq/coq/issues/10679. This commit makes
PG compilation compatible with Coq after that PR. However, the
patch only checks for the Coq version, therefore making PG vio2vo
compilation fail on 8.10 versions before PR 8690. (Compilation
still works, it's just that vio2vo postprocessing for the mode
quick-and-vio2vo fails.)
| -rw-r--r-- | coq/coq-par-compile.el | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index ac2e82bf..c700533d 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -1482,7 +1482,9 @@ Lock the source file and start the coqdep background process" (get job 'src-file))) (message "vio2vo %s" (get job 'src-file)) (coq-par-start-process - coq-prog-name + ;; in 8.9.1 and before only coqtop accepts -schedule-vio2vo + ;; after change 103f59e only coqc accepts -schedule-vio2vo + (if (coq--post-v810) coq-compiler coq-prog-name) (nconc arguments (list "-schedule-vio2vo" "1" module)) 'coq-par-vio2vo-continuation job |