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

fix(frontends/lean/server): compilation warning

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-27 17:53:00 -07:00
parent 1011a8022c
commit 8df5fc0623
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -98,7 +98,7 @@ server::worker::worker(environment const & env, io_state const & ios, definition
io_state _ios(ios); io_state _ios(ios);
while (!m_terminate) { while (!m_terminate) {
file_ptr todo_file; file_ptr todo_file;
unsigned todo_linenum; unsigned todo_linenum = 0;
options todo_options; options todo_options;
// wait for next task // wait for next task
while (!m_terminate) { while (!m_terminate) {