diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index 4eb25cf47e..cfe931a361 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -90,6 +90,9 @@ static bool g_initializing = true; extern "C" void lean_io_mark_end_initialization() { g_initializing = false; } +extern "C" obj_res lean_io_initializing(obj_arg) { + return io_result_mk_ok(box(g_initializing)); +} static obj_res mk_file_not_found_error(b_obj_arg fname) { inc(fname); @@ -98,10 +101,6 @@ static obj_res mk_file_not_found_error(b_obj_arg fname) { return io_result_mk_error(lean_mk_io_error_no_file_or_directory(fname, errnum, details)); } -extern "C" obj_res lean_io_initializing(obj_arg) { - return io_result_mk_ok(box(g_initializing)); -} - static lean_external_class * g_io_handle_external_class = nullptr; static void io_handle_finalizer(void * h) {