max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: move function

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-21 08:58:41 -07:00
parent aa6d6c4dda
commit 0de92b069f
1 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/runtime/io.cpp
View file

@ -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) {