diff options
Diffstat (limited to 'Source/Core/CommandLineOptions.ssc')
| -rw-r--r-- | Source/Core/CommandLineOptions.ssc | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index ff901532..6a0c274a 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -987,7 +987,8 @@ namespace Microsoft.Boogie StratifiedInlining = 1;
break;
default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
+ StratifiedInlining = Int32.Parse((!)args[ps.i]);
+ //ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
break;
}
}
|