From db9ef1e82a33029ba1d417fb7d5efc817fa1efd8 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sat, 23 Mar 2024 17:14:02 +0100 Subject: [PATCH] ci: fix goals present tests (commit a6bd8185) These tests did not run until now. --- ci/simple-tests/README.md | 2 +- .../{test-goals-present.el => coq-test-goals-present.el} | 0 ci/simple-tests/coq-test-prelude-correct.el | 2 +- 3 files changed, 2 insertions(+), 2 deletions(-) rename ci/simple-tests/{test-goals-present.el => coq-test-goals-present.el} (100%) diff --git a/ci/simple-tests/README.md b/ci/simple-tests/README.md index 0d3882afe..c949d58d7 100644 --- 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 b/ci/simple-tests/coq-test-goals-present.el similarity index 100% rename from ci/simple-tests/test-goals-present.el rename to 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 index 77676d205..2dca77cef 100644 --- 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)