summaryrefslogtreecommitdiff
path: root/Test/dafny0/runtest.bat
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2011-12-15 11:33:53 +0100
committerGravatar wuestholz <unknown>2011-12-15 11:33:53 +0100
commit079f0583af3aa16cd46ae47b42150f9483a28027 (patch)
tree87cddee8a8ce7e8478c0435f6164cbc424bc2305 /Test/dafny0/runtest.bat
parent3d0f438dfced142ce3c36d15dcb070237014ad8e (diff)
Dafny: Made sure that error locations refer to the Dafny program, even if the /print option is used.
Diffstat (limited to 'Test/dafny0/runtest.bat')
-rw-r--r--Test/dafny0/runtest.bat2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 18c23e55..f1fc0828 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -23,5 +23,5 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy) do (
echo.
echo -------------------- %%f --------------------
- %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
+ %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
)