Skip to content

Commit 1642c0b

Browse files
committed
account for BaseIO changes
1 parent 20b2c5a commit 1642c0b

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/runtime/io.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1554,11 +1554,11 @@ extern "C" LEAN_EXPORT obj_res lean_io_wait(obj_arg t) {
15541554
return lean_task_get_own(t);
15551555
}
15561556

1557-
extern "C" LEAN_EXPORT obj_res lean_io_wait_any(b_obj_arg task_list, obj_arg) {
1557+
extern "C" LEAN_EXPORT obj_res lean_io_wait_any(b_obj_arg task_list) {
15581558
object * t = lean_io_wait_any_core(task_list);
15591559
object * v = lean_task_get(t);
15601560
lean_inc(v);
1561-
return io_result_mk_ok(v);
1561+
return v;
15621562
}
15631563

15641564
extern "C" LEAN_EXPORT obj_res lean_io_exit(uint8_t code) {

0 commit comments

Comments
 (0)