From aceae7a1b28c91d9d71eb6fa2acb227713656c42 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Aug 2013 19:43:47 -0700 Subject: [PATCH] Change policy for adding input to readline history. Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_parser.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) 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); }