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

fix: object may be a boxed scalar

Browse source 
Example: IOError.unexpectedEof
This commit is contained in:
Leonardo de Moura 2020-03-23 12:14:32 -07:00
parent 95c5ccc97d
commit 2efc1855f0
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/builtin_cmds.cpp
View file

@ -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();