diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp index 695083866..71ed4c3da 100644 --- a/src/frontends/lean/lean_parser.cpp +++ b/src/frontends/lean/lean_parser.cpp @@ -1176,10 +1176,9 @@ bool parse_commands_from_stdin(frontend & fe) { input = readline("# "); if (!input) return errors; + add_history(input); std::istringstream strm(input); - if (parse_commands(fe, strm, false, false)) - add_history(input); - else + if (!parse_commands(fe, strm, false, false)) errors = true; free(input); }