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

chore(frontends/lean/server.cpp): add BEGIN/END for WAIT command

Browse source
This commit is contained in:
Soonho Kong 2014-09-08 16:00:59 -07:00
parent bc640510aa
commit c88bfc0c02
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -779,7 +779,9 @@ bool server::operator()(std::istream & in) {
} else if (is_command(g_options, line)) {
show_options();
} else if (is_command(g_wait, line)) {
m_out << "-- BEGINWAIT" << std::endl;
m_worker.wait();
m_out << "-- ENDWAIT" << std::endl;
} else if (is_command(g_show, line)) {
show(false);
} else if (is_command(g_valid, line)) {