ci: fix goals present tests (commit a6bd818)

These tests did not run until now.
ProofGeneral · Mar 23, 2024 · db9ef1e · db9ef1e
1 parent 728bd25
commit db9ef1e
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 2 deletions.
diff --git a/ci/simple-tests/README.md b/ci/simple-tests/README.md
@@ -12,7 +12,7 @@ coq-test-par-job-needs-compilation-quick
   possible cases
 coq-test-prelude-correct
 : test that the Proof General prelude is correct
-test-goals-present
+coq-test-goals-present
 : test that Proof General shows goals correctly in various
   situations
 

diff --git a/ci/simple-tests/test-goals-present.el → ci/simple-tests/coq-test-goals-present.el b/ci/simple-tests/test-goals-present.el → ci/simple-tests/coq-test-goals-present.el
diff --git a/ci/simple-tests/coq-test-prelude-correct.el b/ci/simple-tests/coq-test-prelude-correct.el
@@ -27,7 +27,7 @@
 (defconst coq--post-v810 (coq--post-v810)
   "t if Coq is more recent than 8.9")
 
-(message "goal present tests run with Coq version %s; post-v810: %s"
+(message "prelude tests run with Coq version %s; post-v810: %s"
          (coq-version t) coq--post-v810)