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

fix: closes #109

Browse source 
Fixed myself after wasting time wondering whether a segfault was
coming from today.

cc @cipher1024
This commit is contained in:
Leonardo de Moura 2020-02-05 09:16:33 -08:00
parent 92d8688880
commit 660571ab38
1 changed files with 4 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/runtime/io.cpp
View file

@ -100,12 +100,10 @@ extern "C" void lean_io_mark_end_initialization() {
}
static obj_res mk_file_not_found_error(b_obj_arg fname) {
object * err = mk_string("file '");
err = string_append(err, fname);
object * tmp = mk_string("' not found");
err = string_append(err, tmp);
dec_ref(tmp);
return set_io_error(err);
inc(fname);
int errnum = ENOENT;
object * details = mk_string("");
return set_io_error(lean_mk_io_error_no_file_or_directory(fname, errnum, details));
}
extern "C" obj_res lean_io_prim_read_text_file(b_obj_arg fname, obj_arg) {