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

fix(frontends/lean/dependencies): warning message

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-31 19:59:05 -07:00
parent f39b2eb70f
commit 466dd11d1b
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/dependencies.cpp
View file

@ -20,10 +20,12 @@ void display_deps(environment const & env, std::ostream & out, char const * fnam
scanner s(in, fname); scanner s(in, fname);
bool import_args = false; bool import_args = false;
while (true) { while (true) {
scanner::token_kind t; scanner::token_kind t = scanner::token_kind::Identifier;
try { try {
t = s.scan(env); t = s.scan(env);
} catch (exception &) {} } catch (exception &) {
continue;
}
if (t == scanner::token_kind::Eof) { if (t == scanner::token_kind::Eof) {
return; return;
} else if (t == scanner::token_kind::CommandKeyword && s.get_token_info().value() == import) { } else if (t == scanner::token_kind::CommandKeyword && s.get_token_info().value() == import) {