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

chore(shell/lean): set new IR compiler as the default

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-23 18:27:41 -07:00
parent c6f717e55b
commit f72d54c2a0
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/shell/lean.cpp
View file

@ -226,7 +226,7 @@ static struct option g_long_options[] = {
{"deps", no_argument, 0, 'd'},
{"timeout", optional_argument, 0, 'T'},
{"cpp", optional_argument, 0, 'c'},
{"newcpp", optional_argument, 0, 'C'}, // temporary flag for testing new IR
{"oldcpp", optional_argument, 0, 'C'}, // use old IR compiler
#if defined(LEAN_JSON)
{"json", no_argument, 0, 'J'},
{"path", no_argument, 0, 'p'},
@ -353,10 +353,10 @@ int main(int argc, char ** argv) {
case 'h':
display_help(std::cout);
return 0;
case 'c':
case 'C':
cpp_output = optarg;
break;
case 'C':
case 'c':
new_cpp_output = optarg;
break;
case 's':