[nongnu] elpa/proof-general dd8f8b4034 1/2: CI compile tests: expect 008-default-dir to fail for 8.15.0

[ELPA Syncer]

branch: elpa/proof-general
commit dd8f8b403401825bbf6c5f80c43f4b0188b620d4
Author: Hendrik Tews <hendrik@askra.de>
Commit: hendriktews <hendrik@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)