summaryrefslogtreecommitdiff
path: root/Test/runTests.bat
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-06-08 18:14:53 -0700
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-06-08 18:14:53 -0700
commit52b326d009545af9dbf44ec54e7ce9d610414517 (patch)
tree4cc0203adb411770c9d4ba4d3330dfa8aa61419c /Test/runTests.bat
parentdd8117ebb70bdb1531a35eb47f490929a5c658fb (diff)
Add the beginning of a new testing infrastructure
runTests.py reads lit-style annotations, so we will be able to retain lit compatibility. This new framework adds: * Precise timings * Proper support for interrupting using Ctrl+C * Much better reporting (including tracking of error codes, and merging of successive reports for performance tracking) * No dependency on lit, OutputCheck, or Diff * Pretty colors!
Diffstat (limited to 'Test/runTests.bat')
-rw-r--r--Test/runTests.bat2
1 files changed, 2 insertions, 0 deletions
diff --git a/Test/runTests.bat b/Test/runTests.bat
new file mode 100644
index 00000000..4eeed06b
--- /dev/null
+++ b/Test/runTests.bat
@@ -0,0 +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 %*