From d8bb4df96f37da29d8c10dce47d47398ae0735ae Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 3 Nov 2019 19:44:49 +0100 Subject: [PATCH] chore: revert "chore: add `std::cout.flush`" This reverts commit a43a225013fdb2748add578eb9bc870e4bee381f. --- src/runtime/io.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index 02be4b5bca..60e62c2ebc 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -94,7 +94,6 @@ 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)); }