From 24a6ee1810fd19f21a22b22033c82fa77dae254c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 25 Oct 2020 09:12:19 -0700 Subject: [PATCH] chore: use new frontend by default --- 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 e5560251cb..ee8f2f0248 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -434,7 +434,7 @@ int main(int argc, char ** argv) { bool use_stdin = false; unsigned trust_lvl = LEAN_BELIEVER_TRUST_LEVEL + 1; bool only_deps = false; - bool new_frontend = false; + bool new_frontend = true; bool stats = false; unsigned num_threads = 0; #if defined(LEAN_MULTI_THREAD)