chore(frontends/lean/server): remove leftover
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
3d8477f7de
commit
92ab2dac83
1 changed files with 0 additions and 1 deletions
|
@ -149,7 +149,6 @@ void server::process_from(unsigned linenum) {
|
|||
&m_file->m_snapshots, &m_file->m_info);
|
||||
p.set_cache(&m_cache);
|
||||
p();
|
||||
std::cout << "DONE\n";
|
||||
} catch (exception& ex) {}
|
||||
}));
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue