max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-14 17:37:37 -07:00
parent 4f78142ed6
commit 94ea1dc705
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
stage0/src/shell/lean.cpp generated
View file

@ -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<environment, messages> r = run_new_frontend(env, contents, opts, mod_fn);