michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Change policy for adding input to readline history.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-21 19:43:47 -07:00
parent bd3b422158
commit aceae7a1b2
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/lean_parser.cpp
View file

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