From 65243ee8333a99f6461abf417d880a028dc96d91 Mon Sep 17 00:00:00 2001
From: Eelco Dolstra <eelco.dolstra@logicblox.com>
Date: Wed, 20 Aug 2014 21:31:38 +0200
Subject: [PATCH] Flush std::cout before closing stdout

---
 src/libmain/shared.cc | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/libmain/shared.cc b/src/libmain/shared.cc
index 5a740367c..6f2f8c5e4 100644
--- a/src/libmain/shared.cc
+++ b/src/libmain/shared.cc
@@ -319,6 +319,7 @@ RunPager::RunPager()
 RunPager::~RunPager()
 {
     if (pid != -1) {
+        std::cout.flush();
         close(STDOUT_FILENO);
         pid.wait(true);
     }