From a43a225013fdb2748add578eb9bc870e4bee381f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 29 Oct 2019 11:07:22 -0700
Subject: [PATCH] chore: add `std::cout.flush`

cc @kha
---
 src/runtime/io.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index 60e62c2ebc..02be4b5bca 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -94,6 +94,7 @@ extern "C" obj_res lean_io_initializing(obj_arg) {
 
 extern "C" obj_res lean_io_prim_put_str(b_obj_arg s, obj_arg) {
     std::cout << string_to_std(s); // TODO(Leo): use out handle
+    std::cout.flush();     // TODO(Leo): remove following line. Added for chasing bug
     return set_io_result(box(0));
 }