diff options
Diffstat (limited to 'src/decision/relevancy.h')
| -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; } } |