From 0de92b069fd9942f587c515100c57ced9196f0bc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 21 Sep 2020 08:58:41 -0700 Subject: [PATCH] chore: move function --- src/runtime/io.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) 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) {