diff options
author | Rustan Leino <leino@microsoft.com> | 2012-10-04 19:26:54 -0700 |
---|---|---|
committer | Rustan Leino <leino@microsoft.com> | 2012-10-04 19:26:54 -0700 |
commit | 5558ba719abd8c9f6184e9d1b70afccfec649a6d (patch) | |
tree | 5c0538b126f5980a542eba3b99f9ef59b02a379b /Test/Makefile | |
parent | a4af24114ae44ee34246fdc8bd16ce05d5518c20 (diff) |
Fixed some goof-ups in the test script edits
Changed the test output to make it easier to spot (in the console output) that everything passed with success or if there were any failures
Diffstat (limited to 'Test/Makefile')
-rw-r--r-- | Test/Makefile | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Test/Makefile b/Test/Makefile index 92c67ae4..6e02aed0 100644 --- a/Test/Makefile +++ b/Test/Makefile @@ -7,11 +7,11 @@ all: dafny dafny: $(addprefix rundfy-, $(TESTS)) -show: - @echo $(TESTS) +rundfy-%: + @cmd /c "runtest.bat $* $(FLAGS)" || : long: $(MAKE) TESTS="$(NORMAL) $(LONG)" all -rundfy-%: - @if ls -f $*/*.dfy >/dev/null 2>&1 ; then cmd /c "runtest.bat $* $(FLAGS)" ; fi || : +show: + @echo $(TESTS) |