summaryrefslogtreecommitdiff
path: root/Test/Makefile
diff options
context:
space:
mode:
authorGravatar MichalMoskal <unknown>2011-02-18 22:04:49 +0000
committerGravatar MichalMoskal <unknown>2011-02-18 22:04:49 +0000
commit83bd938cd65b0d64ed72e45411c02563b0d3a3de (patch)
tree722d4cfd793c9118bf9f77c88c948ea73b3e1e54 /Test/Makefile
parent2e4c60cba8c332250ee1a88fa62744eec0034763 (diff)
Allow for running Boogie and Dafny testcases separately
Diffstat (limited to 'Test/Makefile')
-rw-r--r--Test/Makefile7
1 files changed, 6 insertions, 1 deletions
diff --git a/Test/Makefile b/Test/Makefile
index 5b43a7af..87e27f23 100644
--- a/Test/Makefile
+++ b/Test/Makefile
@@ -6,6 +6,8 @@ TESTS = $(NORMAL)
all: $(addprefix run-, $(TESTS))
@echo ALL OK
+dafny: $(addprefix rundfy-, $(TESTS))
+ @echo ALL OK
show:
@echo $(TESTS)
@@ -14,4 +16,7 @@ long:
$(MAKE) TESTS="$(NORMAL) $(LONG)" all
run-%:
- @./runtest.bat $* $(FLAGS)
+ @if ls -f $*/*.dfy >/dev/null 2>&1 ; then true ; else ./runtest.bat $* $(FLAGS) ; fi
+
+rundfy-%:
+ @if ls -f $*/*.dfy >/dev/null 2>&1 ; then ./runtest.bat $* $(FLAGS) ; fi