branch: elpa/proof-general
commit dd8f8b403401825bbf6c5f80c43f4b0188b620d4
Author: Hendrik Tews <hend...@askra.de>
Commit: hendriktews <hend...@askra.de>
CI compile tests: expect 008-default-dir to fail for 8.15.0
See Coq issue 15773.
---
ci/compile-tests/008-default-dir/runtest.el | 14 ++++++++++++--
1 file changed, 12 insertions(+), 2 deletions(-)
diff --git a/ci/compile-tests/008-default-dir/runtest.el
b/ci/compile-tests/008-default-dir/runtest.el
index e4c3f4e184..42bf61a4e4 100644
--- a/ci/compile-tests/008-default-dir/runtest.el
+++ b/ci/compile-tests/008-default-dir/runtest.el
@@ -13,7 +13,12 @@
;; ert tests for parallel background compilation for Coq
;;
;; Test that default-directory is correctly set independently of the
-;; current buffer in the foreground.
+;; current buffer in the foreground, both for first and second stage
+;; compilation.
+;;
+;; This test fails for Coq 8.15.0, because the test checks .vok files,
+;; which, in certain situations, are not created by that coq version.
+;; See Coq issue 15773.
;;
;; The dependencies in this test are:
;;
@@ -60,9 +65,14 @@ See `cct-generic-check-main-buffer'."
;;; The test itself
(ert-deftest test-default-dir ()
+ :expected-result (if (equal (coq-version t) "8.15.0") :failed :passed)
"`default-directory' test.
Test that `default-directory' is correctly set independently of the
-current buffer in the foreground."
+current buffer in the foreground.
+
+This test fails for Coq 8.15.0, because the test checks .vok
+files, which are not created by that coq version, in certain
+situations. See Coq issue 15773."
(let (vo-times av-buffer ci-buffer other-locked-files
vok-times vos-vio-files)
