2 files changed, 24 insertions, 6 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()
 {
diff --git a/tools/standalone_miri/debug.hpp b/tools/standalone_miri/debug.hpp
index b3b0d76f..4b8d7aa9 100644
--- a/tools/standalone_miri/debug.hpp
+++ b/tools/standalone_miri/debug.hpp
@@ -21,17 +21,26 @@ enum class DebugLevel {
     Bug,
 };
 
-class DebugSink
+class DebugSink//:
+    //public ::std::ostream
 {
     static unsigned s_indent;
     static ::std::unique_ptr<std::ofstream> s_out_file;
     ::std::ostream& m_inner;
-    DebugSink(::std::ostream& inner);
+    bool m_stderr_too;
+    DebugSink(::std::ostream& inner, bool stderr_too);
 public:
     ~DebugSink();
 
     template<typename T>
-    ::std::ostream& operator<<(const T& v) { return m_inner << v; }
+    DebugSink& operator<<(const T& v) {
+        if( m_stderr_too )
+        {
+            ::std::cerr << v;
+        }
+        m_inner << v;
+        return *this;
+    }
 
     static void set_output_file(const ::std::string& s);
     static bool enabled(const char* fcn_name);