summaryrefslogtreecommitdiff
path: root/test/regress/regress0/lemmas
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-11-15 20:08:17 +0000
committerMorgan Deters <mdeters@gmail.com>2010-11-15 20:08:17 +0000
commit80596bc6e2a4aba6c14d408a41a214579b636f03 (patch)
tree17a09dc22f5bf10c7008e0b8467052ae92112149 /test/regress/regress0/lemmas
parent0eb2a0362fee06023f0668e94bb566b69f4a7cda (diff)
fix some things with the build system (make dist, make install, make check)
Diffstat (limited to 'test/regress/regress0/lemmas')
-rw-r--r--test/regress/regress0/lemmas/Makefile8
1 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/regress0/lemmas/Makefile b/test/regress/regress0/lemmas/Makefile
new file mode 100644
index 000000000..96e24225b
--- /dev/null
+++ b/test/regress/regress0/lemmas/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/lemmas
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback