diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-14 13:47:33 +0000 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-14 13:47:33 +0000 |
| commit | c1b87cb541768fa9811cef643e43fdc09091c353 (patch) | |
| tree | 4c5ce6775b34e9949277ed95fa841fba6dab0fc9 /src/decision | |
| parent | 389863844682473d0b5b84b3a8288282909e15d2 (diff) | |
fix cout, fix statname, rm deadcode
Diffstat (limited to 'src/decision')
| -rw-r--r-- | src/decision/relevancy.h | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h index 93fb3c999..3a33a5cb8 100644 --- a/src/decision/relevancy.h +++ b/src/decision/relevancy.h @@ -255,9 +255,7 @@ public: // we are becuase of not getting information about literals // created using newLiteral command... need to figure how to // handle that - Warning() << "isRelevant: WARNING: didn't find node when we should had" << std::endl; - // Warning() doesn't work for some reason - cout << "isRelevant: WARNING: didn't find node when we should had" << std::endl; + Message() << "isRelevant: WARNING: didn't find node when we should had" << std::endl; } } |