diff options
Diffstat (limited to 'Test/snapshots/runtest.bat')
| -rw-r--r-- | Test/snapshots/runtest.bat | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/Test/snapshots/runtest.bat b/Test/snapshots/runtest.bat deleted file mode 100644 index 7821e39c..00000000 --- a/Test/snapshots/runtest.bat +++ /dev/null @@ -1,8 +0,0 @@ -@echo off
-setlocal
-
-set BOOGIEDIR=..\..\Binaries
-set BGEXE=%BOOGIEDIR%\Boogie.exe
-
-%BGEXE% %* /verifySnapshots /verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl
-
|