From 94ea1dc70570d40d3808d510ef3af83b8204e89a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 Oct 2020 17:37:37 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/shell/lean.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/stage0/src/shell/lean.cpp b/stage0/src/shell/lean.cpp index 7bbd8eb08c..d21fdadf2f 100644 --- a/stage0/src/shell/lean.cpp +++ b/stage0/src/shell/lean.cpp @@ -628,6 +628,10 @@ int main(int argc, char ** argv) { contents.erase(0, end_line_pos); } + // Temporary HACK until we add support for `--deps` using the new frontend + if (only_deps) + new_frontend = false; + bool ok = true; if (new_frontend) { pair_ref r = run_new_frontend(env, contents, opts, mod_fn);