From 1f0171cd57cca127605b2495fb61cb2538b24f20 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 29 Jun 2014 09:55:30 -0700 Subject: [PATCH] fix(frontends/lean/dependencies): compilation warning Signed-off-by: Leonardo de Moura --- src/frontends/lean/dependencies.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/frontends/lean/dependencies.cpp b/src/frontends/lean/dependencies.cpp index e38376407..94723ed87 100644 --- a/src/frontends/lean/dependencies.cpp +++ b/src/frontends/lean/dependencies.cpp @@ -22,11 +22,11 @@ bool consume_until_import(environment const & env, scanner & s) { while (true) { try { t = s.scan(env); + if (t == scanner::token_kind::Eof) + return false; + if (t == scanner::token_kind::CommandKeyword && s.get_token_info().value() == import) + return true; } catch (...) {} - if (t == scanner::token_kind::Eof) - return false; - if (t == scanner::token_kind::CommandKeyword && s.get_token_info().value() == import) - return true; } }