summaryrefslogtreecommitdiff
path: root/Test/VSI-Benchmarks/runtest.bat
diff options
context:
space:
mode:
authorGravatar Dan Rosén <danr@chalmers.se>2014-07-07 17:24:46 -0700
committerGravatar Dan Rosén <danr@chalmers.se>2014-07-07 17:24:46 -0700
commit661faf59f8e1003cdbf339260d1293e8dd77f2df (patch)
tree37e11e8a86658fe4d69b38572f3b6fadd8d287c9 /Test/VSI-Benchmarks/runtest.bat
parent8de9fcae1a91acce9a1e59f292f05a95c81b3dbc (diff)
parent93d9965a347b1a6ad70007822f01c2b032ea5436 (diff)
Merge
Diffstat (limited to 'Test/VSI-Benchmarks/runtest.bat')
-rw-r--r--Test/VSI-Benchmarks/runtest.bat13
1 files changed, 0 insertions, 13 deletions
diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat
deleted file mode 100644
index f950cf2a..00000000
--- a/Test/VSI-Benchmarks/runtest.bat
+++ /dev/null
@@ -1,13 +0,0 @@
-@echo off
-setlocal
-
-set BINARIES=..\..\Binaries
-set DAFNY_EXE=%BINARIES%\Dafny.exe
-
-%DAFNY_EXE% /compile:0 /verifySeparately %* b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy
-
-rem for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (
-rem echo.
-rem echo -------------------- %%f --------------------
-rem %DAFNY_EXE% /compile:0 %* %%f
-rem )