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)); }