From b624b7d03f85d81abec9c42008b6fddb3cec0c4c Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 31 Aug 2020 11:05:54 +0200
Subject: [PATCH] chore: remove obsolete header

---
 src/include/lean/lean.h | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index be6f246582..40c378bb93 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -1771,7 +1771,6 @@ static inline lean_obj_res lean_io_result_mk_ok(lean_obj_arg a) {
     lean_ctor_set(r, 1, lean_box(0));
     return r;
 }
-static inline lean_obj_res lean_mk_io_result(lean_obj_arg a) { return lean_io_result_mk_ok(a); }
 static inline lean_obj_res lean_io_result_mk_error(lean_obj_arg e) {
     lean_object * r = lean_alloc_ctor(1, 2, 0);
     lean_ctor_set(r, 0, e);