diff --git a/src/init/init.cpp b/src/init/init.cpp index c945814e95..4ef0706e25 100644 --- a/src/init/init.cpp +++ b/src/init/init.cpp @@ -38,7 +38,6 @@ void initialize() { initialize_frontend_lean_module(); object * w = initialize_init_default(io_mk_world()); w = initialize_init_lean_default(w); - lean::io_mark_end_initialization(); if (io_result_is_error(w)) { io_result_show_error(w); dec(w); @@ -84,6 +83,7 @@ void finalize() { initializer::initializer() { initialize(); + lean::io_mark_end_initialization(); } initializer::~initializer() { diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index 1497447dce..eb4b162b43 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -56,7 +56,9 @@ static obj_res option_of_io_result(obj_arg r) { } static bool g_initializing = true; -void io_mark_end_initialization() { g_initializing = false; } +void io_mark_end_initialization() { + g_initializing = false; +} extern "C" obj_res lean_io_initializing(obj_arg r) { return set_io_result(r, box(g_initializing));