From c78bf115248f62fa355e7a9b2b9532b37e693085 Mon Sep 17 00:00:00 2001
From: Eelco Dolstra <e.dolstra@tudelft.nl>
Date: Thu, 16 Oct 2003 11:55:37 +0000
Subject: [PATCH] * Enable buffering of stderr in C++.

---
 src/shared.cc | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/shared.cc b/src/shared.cc
index 32e8916175..dcda0b50ab 100644
--- a/src/shared.cc
+++ b/src/shared.cc
@@ -53,6 +53,10 @@ int main(int argc, char * * argv)
     ATerm bottomOfStack;
     ATinit(argc, argv, &bottomOfStack);
 
+    /* Turn on buffering for cerr. */
+    char buf[1024];
+    cerr.rdbuf()->pubsetbuf(buf, sizeof(buf));
+
     try {
         initAndRun(argc, argv);
     } catch (UsageError & e) {