branch: elpa/proof-general
commit d2d1a73f2b93937a5f0abd6d93aa810d1f72b419
Author: Stefan Monnier <monn...@iro.umontreal.ca>
Commit: Erik Martin-Dorel <erik.martin-do...@irit.fr>
Minor tweaks encountered while trying to run the CI tests
* ci/coq-tests.el (070_coq-test-regression-wholefile-no-proof):
Clarify the intention of the test.
* Makefile (check): Fix comment.
(tests): New target.
* .gitignore: Add `ci/.lia.cache`, apparently generated by ci/test.sh
---
.gitignore | 1 +
Makefile | 14 +++++++++-----
ci/coq-tests.el | 2 +-
3 files changed, 11 insertions(+), 6 deletions(-)
diff --git a/.gitignore b/.gitignore
index 2039757..0af17ea 100644
--- a/.gitignore
+++ b/.gitignore
@@ -5,3 +5,4 @@ ChangeLog
proof-general-autoloads.el
*.elc
*~
+/ci/.lia.cache
diff --git a/Makefile b/Makefile
index 265aad6..668241b 100644
--- a/Makefile
+++ b/Makefile
@@ -9,6 +9,7 @@
## make scripts - edit paths to bash/perl/PGHOME in scripts
## make install - install into system directories
## make clean - return to clean source
+## make tests - run the suite of regression tests
##
## Edit the EMACS setting below or call with an explicit one, like this:
##
@@ -103,14 +104,12 @@ compile: $(EL)
@echo "****************************************************************"
##
-## compile : byte compile all lisp files
-##
-## Compiling can show up errors in the code, but be wary of fixing obsoletion
-## or argument call warnings unless they're valid for all supported Emacsen.
+## check : make sure compilation doesn't emit warnings
##
## The check target aborts compilation on any byte-compiler warning.
-## Compile with this target once before commiting your changes to
+## Compile with this target once before commiting your changes to
## the repository.
+## FIXME: Compilation currently emits many warnings :-(
##
check: $(EL)
@echo "****************************************************************"
@@ -121,6 +120,11 @@ check: $(EL)
@echo " Finished."
@echo "****************************************************************"
+##
+## tests : run regression tests
+##
+tests:
+ ci/test.sh
##
## Make an individual .elc. Building separately means we need to be
diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index ff762d9..fb5635f 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -274,7 +274,7 @@ For example, COMMENT could be (*test-definition*)"
(proof-shell-wait)
(goto-char (point-min))
(insert "(*.*)")
- (should (equal (proof-queue-or-locked-end) 1)))))
+ (should (equal (proof-queue-or-locked-end) (point-min))))))
(ert-deftest 080_coq-test-regression-show-proof-stepwise()
"Regression test for the \"Show Proof\" option"
