diff options
author | 2011-02-11 19:37:21 +0000 | |
---|---|---|
committer | 2011-02-11 19:37:21 +0000 | |
commit | 3b7e0b36496f504ae62acc61294d5b399feaf11c (patch) | |
tree | 33238eee9da81252a6f3073b2cd3aa09f3780e68 /Source/Core/Util.cs | |
parent | 42d1d5646c440eb2b8441a7ce292bc7193b7409c (diff) |
Get rid of some warnings.
Diffstat (limited to 'Source/Core/Util.cs')
-rw-r--r-- | Source/Core/Util.cs | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index f6c94ee2..6bf0da30 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -18,7 +18,6 @@ namespace Microsoft.Boogie { Contract.Invariant(writer != null);
}
- bool writerOpenedHere = false;
bool setTokens = true;
int line = 1;
int col;
@@ -111,7 +110,6 @@ namespace Microsoft.Boogie { Contract.Requires(filename != null);
this.filename = filename;
this.writer = new StreamWriter(filename);
- this.writerOpenedHere = true;
//base();
}
|