diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index 38bfa4bbbb..7c02e2fe1b 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -282,17 +282,15 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_flush(b_obj_arg h, obj_arg /*
 /* Handle.read : (@& Handle) → USize → IO ByteArray */
 extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_read(b_obj_arg h, usize nbytes, obj_arg /* w */) {
     FILE * fp = io_get_handle(h);
-    if (feof(fp)) {
-        return io_result_mk_ok(alloc_sarray(1, 0, 0));
-    }
     obj_res res = lean_alloc_sarray(1, 0, nbytes);
     usize n = std::fread(lean_sarray_cptr(res), 1, nbytes, fp);
     if (n > 0) {
         lean_sarray_set_size(res, n);
         return io_result_mk_ok(res);
     } else if (feof(fp)) {
-        dec_ref(res);
-        return io_result_mk_ok(alloc_sarray(1, 0, 0));
+        clearerr(fp);
+        lean_sarray_set_size(res, n);
+        return io_result_mk_ok(res);
     } else {
         dec_ref(res);
         return io_result_mk_error(decode_io_error(errno, nullptr));