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);