aboutsummaryrefslogtreecommitdiff
path: root/ci/compile-tests/007-slow-require/Makefile
blob: b99eebc1dc864e41966f01e1bfa1680158fc1983 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
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)