From fc4abbd6c3ecf5e84707c1e48224d22bb7f17be7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Jun 2019 10:42:39 -0700 Subject: [PATCH] chore(shell/lean): compilation warning --- src/shell/lean.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 6bc6163916..016b9e0c14 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -503,7 +503,7 @@ int main(int argc, char ** argv) { return 0; } - bool ok; + bool ok = true; if (new_frontend) { #if 0 env.set_main_module(main_module_name);