From 095d100a382c3d786b9fd7d93a8caeea5f05fabe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 May 2018 11:09:07 -0700 Subject: [PATCH] chore(util/debug): remove logtree dependency --- src/util/debug.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/util/debug.cpp b/src/util/debug.cpp index 7cdd684698..8e26e8a7f2 100644 --- a/src/util/debug.cpp +++ b/src/util/debug.cpp @@ -18,7 +18,7 @@ Author: Leonardo de Moura #include #endif #include "util/debug.h" -#include "util/log_tree.h" +// #include "util/log_tree.h" namespace lean { static volatile bool g_has_violations = false; @@ -49,8 +49,8 @@ void notify_assertion_violation(const char * fileName, int line, const char * co std::cerr << "LEAN ASSERTION VIOLATION\n"; std::cerr << "File: " << fileName << "\n"; std::cerr << "Line: " << line << "\n"; - if (has_logtree()) - std::cerr << "Task: " << logtree().get_location().m_file_name << ": " << logtree().get_description() << "\n"; + // if (has_logtree()) + // std::cerr << "Task: " << logtree().get_location().m_file_name << ": " << logtree().get_description() << "\n"; std::cerr << condition << "\n"; std::cerr.flush(); }