summaryrefslogtreecommitdiff
path: root/Makefile.builds.in
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-12-12 18:24:54 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2013-12-16 22:28:26 -0500
commit5186ca79710fe935d1f7ed27c4a34e913ab547e8 (patch)
tree4f5ce4957063085f607492a6474b0d244e4b2da4 /Makefile.builds.in
parent4d9caf9782c59823fb95519b9b518b7d7f89738a (diff)
First attempt at incorporating LFSC proof checker into CVC4.
Diffstat (limited to 'Makefile.builds.in')
-rw-r--r--Makefile.builds.in4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.builds.in b/Makefile.builds.in
index 33df24f95..296e5a974 100644
--- a/Makefile.builds.in
+++ b/Makefile.builds.in
@@ -192,12 +192,12 @@ endif
# The descent into "src" with target "check" is to build check
# prerequisites (e.g. CHECK_PROGRAMS, CHECK_LTLIBRARIES, ...).
-check test units:
+check test units: all
(cd $(CURRENT_BUILD)/src && $(MAKE) check)
+(cd $(CURRENT_BUILD)/test && $(MAKE) $@)
systemtests regress: all
+(cd $(CURRENT_BUILD)/test && $(MAKE) $@)
-units%:
+units%: all
(cd $(CURRENT_BUILD)/src && $(MAKE) check)
+(cd $(CURRENT_BUILD)/test && $(MAKE) units TEST_PREFIX=$(subst units:,,$@))
regress%: all
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback