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

feat(shell/lean): trap 'std::bad_alloc' and print nicer error message

Browse source 
See #489
This commit is contained in:
Leonardo de Moura 2015-04-20 17:55:00 -07:00
parent 47e37a3353
commit 68d4978953
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/shell/lean.cpp
View file

@ -604,6 +604,9 @@ int main(int argc, char ** argv) {
return ok ? 0 : 1; return ok ? 0 : 1;
} catch (lean::throwable & ex) { } catch (lean::throwable & ex) {
lean::display_error(diagnostic(env, ios), nullptr, ex); lean::display_error(diagnostic(env, ios), nullptr, ex);
} catch (std::bad_alloc & ex) {
std::cerr << "out of memory" << std::endl;
return 1;
} }
return 1; return 1;
} }