diff options
Diffstat (limited to 'Source/Core/CommandLineOptions.cs')
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 3324d632..eadd8b97 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -351,6 +351,7 @@ namespace Microsoft.Boogie { public int StratifiedInliningOption = 0;
public int RecursionBound = 500;
public string CoverageReporterPath = null;
+ public Process coverageReporter = null; // used internally for debugging
public enum TypeEncoding {
None,
|