diff options
Diffstat (limited to 'Test/runtestdafny.bat')
| -rw-r--r-- | Test/runtestdafny.bat | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/Test/runtestdafny.bat b/Test/runtestdafny.bat deleted file mode 100644 index df633681..00000000 --- a/Test/runtestdafny.bat +++ /dev/null @@ -1,8 +0,0 @@ -@echo off
-setlocal
-
-set errors=0
-
-for /F "eol=; tokens=1,2,3*" %%i in (dafnytests.txt) do if %%j==Use call runtest.bat %%i %1 %2 %3 %4 %5 %6 %7 %8 %9 || set errors=1
-
-exit /b %errors%
|