From 466dd11d1b1b3b6d9e862acad8a4355c2588f508 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 31 Jul 2014 19:59:05 -0700 Subject: [PATCH] fix(frontends/lean/dependencies): warning message Signed-off-by: Leonardo de Moura --- src/frontends/lean/dependencies.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/dependencies.cpp b/src/frontends/lean/dependencies.cpp index f50e89543..665a7e1b3 100644 --- a/src/frontends/lean/dependencies.cpp +++ b/src/frontends/lean/dependencies.cpp @@ -20,10 +20,12 @@ void display_deps(environment const & env, std::ostream & out, char const * fnam scanner s(in, fname); bool import_args = false; while (true) { - scanner::token_kind t; + scanner::token_kind t = scanner::token_kind::Identifier; try { t = s.scan(env); - } catch (exception &) {} + } catch (exception &) { + continue; + } if (t == scanner::token_kind::Eof) { return; } else if (t == scanner::token_kind::CommandKeyword && s.get_token_info().value() == import) {