michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(shell): use --server for .hlean files

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-05 16:13:29 -08:00
parent 53d6d76162
commit effbf78d36
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/shell/lean.cpp
View file

@ -515,7 +515,7 @@ int main(int argc, char ** argv) {
lean::display_error(diagnostic(env, ios), &pp, ex);
}
}
if (ok && server && default_k == input_kind::Lean) {
if (ok && server && (default_k == input_kind::Lean || default_k == input_kind::HLean)) {
signal(SIGINT, on_ctrl_c);
ios.set_option(lean::name("pp", "beta"), true);
lean::server Sv(env, ios, num_threads);