diff options
Diffstat (limited to 'ci/compile-tests/005-change-recompile/Makefile')
| -rw-r--r-- | ci/compile-tests/005-change-recompile/Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ci/compile-tests/005-change-recompile/Makefile b/ci/compile-tests/005-change-recompile/Makefile index 983227be..4cdc6503 100644 --- a/ci/compile-tests/005-change-recompile/Makefile +++ b/ci/compile-tests/005-change-recompile/Makefile @@ -17,8 +17,8 @@ TEST_SOURCES:=a.v b.v c.v d.v e.v f.v g.v h.v 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 + emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \ + -l runtest.el -f ert-run-tests-batch-and-exit %.v: %.v.orig cp $< $@ |