diff options
Diffstat (limited to 'ci/compile-tests/007-slow-require/Makefile')
| -rw-r--r-- | ci/compile-tests/007-slow-require/Makefile | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/ci/compile-tests/007-slow-require/Makefile b/ci/compile-tests/007-slow-require/Makefile new file mode 100644 index 00000000..b99eebc1 --- /dev/null +++ b/ci/compile-tests/007-slow-require/Makefile @@ -0,0 +1,35 @@ +# This file is part of Proof General. +# +# © Copyright 2021 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:=\ + a1.v b1.v c1.v d1.v \ + a2.v b2.v c2.v d2.v \ + a3.v b3.v c3.v d3.v \ + a4.v b4.v c4.v d4.v \ + a5.v b5.v c5.v d5.v \ + a6.v b6.v c6.v d6.v + +.PHONY: test +test: + $(MAKE) clean + $(MAKE) $(TEST_SOURCES) + emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \ + -l runtest.el -f ert-run-tests-batch-and-exit \ + 9>&1 + +%.v: %.v.orig + cp $< $@ + +.PHONY: clean +clean: + rm -f *.vo *.glob *.vio *.vos *.vok .*.aux $(TEST_SOURCES) |