diff options
| author | Hendrik Tews | 2020-12-14 22:27:36 +0100 |
|---|---|---|
| committer | hendriktews | 2020-12-19 16:43:49 +0100 |
| commit | 7cde26b20cab22d2a82f6bb50e852bbb5688d610 (patch) | |
| tree | 9cb9181b1d7c0d2601f7d7b7edc4415e58111deb /ci/compile-tests/006-ready-dependee/Makefile | |
| parent | 16e784a63f2a38ce3f03e36b6fa9a7db2da211b9 (diff) | |
add auto compile test to trigger two bugs for dependees in state ready
See also the committed test.el. The test is not completely
robust, it needs to be improved in the future.
Diffstat (limited to 'ci/compile-tests/006-ready-dependee/Makefile')
| -rw-r--r-- | ci/compile-tests/006-ready-dependee/Makefile | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/ci/compile-tests/006-ready-dependee/Makefile b/ci/compile-tests/006-ready-dependee/Makefile new file mode 100644 index 00000000..fe014bfc --- /dev/null +++ b/ci/compile-tests/006-ready-dependee/Makefile @@ -0,0 +1,28 @@ +# This file is part of Proof General. +# +# © Copyright 2020 Hendrik Tews +# +# Authors: Hendrik Tews +# Maintainer: Hendrik Tews <hendrik@askra.de> +# +# License: GPL (GNU GENERAL PUBLIC LICENSE) + + +# This test modifies some .v files during the test. The original +# versions are in .v.orig files. They are moved to the corresponding +# .v files before the test starts. +TEST_SOURCES:=a.v b.v c.v d.v e.v f.v g.v h.v i.v j.v k.v + +.PHONY: test +test: + $(MAKE) clean + $(MAKE) $(TEST_SOURCES) + emacs -batch -l ert -l ../../../generic/proof-site.el -l ../cct-lib.el \ + -l test.el -f ert-run-tests-batch-and-exit + +%.v: %.v.orig + cp $< $@ + +.PHONY: clean +clean: + rm -f *.vo *.glob *.vio *.vos *.vok .*.aux $(TEST_SOURCES) |