diff options
Diffstat (limited to 'Test/runtest.bat')
| -rw-r--r-- | Test/runtest.bat | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Test/runtest.bat b/Test/runtest.bat index 5b3d45ae..8a75f363 100644 --- a/Test/runtest.bat +++ b/Test/runtest.bat @@ -5,7 +5,12 @@ if not exist %1\nul goto noDirExists echo ----- Running regression test %1
pushd %1
if not exist runtest.bat goto noRunTest
+if "%1" == "dafnyCompiler" goto compilerTests
call runtest.bat -nologo -logPrefix:%* > Output
+goto Continue
+:compilerTests
+call runtestall.bat > Output
+:Continue
rem There seem to be some race between finishing writing to the Output file, and running fc.
rem Calling fc twice seems to fix (or at least alleviate) the problem.
fc /W Answer Output > nul
|