summaryrefslogtreecommitdiff
path: root/Test/runTests.bat
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-06-10 16:29:50 -0700
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-06-10 16:29:50 -0700
commitb9ed0285592f5f0d12d02b3d9155dfe46903b6c5 (patch)
treee383447875cc2b4492cc22b8b93ecbfe2fd6f7db /Test/runTests.bat
parent1e9a9af1700f67dde62e8ceb81aa16e13de0e3fb (diff)
Small improvements to runTests.py
Diffstat (limited to 'Test/runTests.bat')
-rw-r--r--Test/runTests.bat2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/runTests.bat b/Test/runTests.bat
index 4eeed06b..ced3bd27 100644
--- a/Test/runTests.bat
+++ b/Test/runTests.bat
@@ -1,2 +1,2 @@
@REM runTests.bat -f "/dprelude PRELUDE_FILE" -r REPORT_NAME INPUT_FILES
-C:/Python34/python.exe runTests.py --compiler "c:/MSR/dafny/Binaries/Dafny.exe /useBaseNameForFileName /compile:1 /nologo" --difftool "C:\Program Files (x86)\Meld\Meld.exe" -j4 %*
+C:/Python34/python.exe runTests.py --flags "/useBaseNameForFileName /compile:1 /nologo" --difftool "C:/Program Files (x86)/Meld/Meld.exe" %*