From 2efc1855f0ca67a727376e04d84faede1d0987f8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 23 Mar 2020 12:14:32 -0700 Subject: [PATCH] fix: object may be a boxed scalar Example: IOError.unexpectedEof --- src/frontends/lean/builtin_cmds.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 0b39432212..a7a3611268 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -405,7 +405,7 @@ static environment eval_cmd(parser & p) { if (io_result_is_error(r.raw())) { message_builder msg = p.mk_message(p.cmd_pos(), p.pos(), ERROR); object * err = io_result_get_error(r.raw()); - inc_ref(err); + inc(err); object * str = lean_io_error_to_string(err); msg << string_to_std(str); msg.report();