summaryrefslogtreecommitdiff
path: root/Test/test20
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/test20
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/test20')
-rw-r--r--Test/test20/TypeSynonyms2.bpl2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/test20/TypeSynonyms2.bpl b/Test/test20/TypeSynonyms2.bpl
index 472b1e96..1cb6e781 100644
--- a/Test/test20/TypeSynonyms2.bpl
+++ b/Test/test20/TypeSynonyms2.bpl
@@ -1,6 +1,6 @@
// RUN: %boogie "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
-// RUN: %boogie -noVerify -print:- -env:0 -printDesugared "%s" > "%t"
+// RUN: %boogie -noVerify -print:- -pretty:0 -env:0 -printDesugared "%s" > "%t"
// RUN: %diff "%s.print.expect" "%t"