diff options
Diffstat (limited to 'lib/Support/ErrorHandling.cpp')
| -rw-r--r-- | lib/Support/ErrorHandling.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/lib/Support/ErrorHandling.cpp b/lib/Support/ErrorHandling.cpp index 5c7b69dd..2f4bc5cc 100644 --- a/lib/Support/ErrorHandling.cpp +++ b/lib/Support/ErrorHandling.cpp @@ -31,8 +31,11 @@ static const char *warningOncePrefix = "WARNING ONCE"; static const char *errorPrefix = "ERROR"; static const char *notePrefix = "NOTE"; -namespace { +namespace klee { cl::OptionCategory MiscCat("Miscellaneous options", ""); +} + +namespace { cl::opt<bool> WarningsOnlyToFile( "warnings-only-to-file", cl::init(false), cl::desc("All warnings will be written to warnings.txt only. If disabled, " |