1 files changed, 12 insertions, 3 deletions
diff --git a/tools/standalone_miri/debug.cpp b/tools/standalone_miri/debug.cpp
index c49df960..be3c9ec4 100644
--- a/tools/standalone_miri/debug.cpp
+++ b/tools/standalone_miri/debug.cpp
@@ -11,14 +11,19 @@
 unsigned DebugSink::s_indent = 0;
 ::std::unique_ptr<std::ofstream> DebugSink::s_out_file;
 
-DebugSink::DebugSink(::std::ostream& inner):
-    m_inner(inner)
+DebugSink::DebugSink(::std::ostream& inner, bool stderr_too):
+    m_inner(inner),
+    m_stderr_too(stderr_too)
 {
 }
 DebugSink::~DebugSink()
 {
     m_inner << "\n";
     m_inner.flush();
+    if( m_stderr_too )
+    {
+        ::std::cerr << ::std::endl;
+    }
 }
 void DebugSink::set_output_file(const ::std::string& s)
 {
@@ -30,6 +35,7 @@ bool DebugSink::enabled(const char* fcn_name)
 }
 DebugSink DebugSink::get(const char* fcn_name, const char* file, unsigned line, DebugLevel lvl)
 {
+    bool stderr_too = false;
     auto& sink = s_out_file ? *s_out_file : ::std::cout;
     for(size_t i = s_indent; i--;)
         sink << " ";
@@ -49,15 +55,18 @@ DebugSink DebugSink::get(const char* fcn_name, const char* file, unsigned line,
         break;
     case DebugLevel::Error:
         sink << "ERROR: ";
+        stderr_too = true;
         break;
     case DebugLevel::Fatal:
         sink << "FATAL: ";
+        stderr_too = true;
         break;
     case DebugLevel::Bug:
         sink << "BUG: " << file << ":" << line << ": ";
+        stderr_too = true;
         break;
     }
-    return DebugSink(sink);
+    return DebugSink(sink, stderr_too);
 }
 void DebugSink::inc_indent()
 {