diff options
| author |  wuestholz <unknown> | 2014-10-15 00:06:15 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-10-15 00:06:15 +0200 |
| commit | d2cc6486f7e5206119035398125270ea2f2c20b2 (patch) | |
| tree | 1838c8c836d9112ead61ed70c1422c232385d6ac /Source/Core/Util.cs | |
| parent | 22160d04342df7a9dec085d235b50875f06f648c (diff) | |
Fix issue in computation of checksums for indented statements.
Diffstat (limited to 'Source/Core/Util.cs')
| -rw-r--r-- | Source/Core/Util.cs | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index 0a2e5a22..06e4fcf0 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -313,7 +313,10 @@ namespace Microsoft.Boogie { }
public void WriteIndent(int level) {
- this.Write(Indent(level));
+ if (!UseForComputingChecksums)
+ {
+ this.Write(Indent(level));
+ }
}
public void Write(string text, params object[] args) {
|