summaryrefslogtreecommitdiff
path: root/Test/test0
diff options
context:
space:
mode:
authorGravatar Dan Rosén <danr@chalmers.se>2014-06-24 10:32:15 -0700
committerGravatar Dan Rosén <danr@chalmers.se>2014-06-24 10:32:15 -0700
commit3f2958db79781cc73938c4e9ed9ba92efcf66f62 (patch)
tree48e678df24ccf700780379a2f737e80625f4235c /Test/test0
parent98bcde1368eb6a5df44cf252e3a2f8d8f509a0df (diff)
Add some pretty-printing, on by default. Turn off with the flag "/pretty:0"
When running boogie form the command line, this should be on by default. On the other hand, the TokenTextWriter constructors and PrintBplFile now have an argument for this, but by default it is off.
Diffstat (limited to 'Test/test0')
-rw-r--r--Test/test0/PrettyPrint.bpl2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/test0/PrettyPrint.bpl b/Test/test0/PrettyPrint.bpl
index 8aa25d33..c79eff80 100644
--- a/Test/test0/PrettyPrint.bpl
+++ b/Test/test0/PrettyPrint.bpl
@@ -1,4 +1,4 @@
-// RUN: %boogie -noVerify -printInstrumented "%s" > "%t"
+// RUN: %boogie -pretty:0 -noVerify -printInstrumented "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
const x: int;
const y: int;