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

fix(shell/lean): check whether output file was created or not

Browse source
This commit is contained in:
Leonardo de Moura 2019-03-18 12:44:00 -07:00
parent 6bd3f1168a
commit d45da2d5ba
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/shell/lean.cpp
View file

@ -546,6 +546,10 @@ int main(int argc, char ** argv) {
if (cpp_output && ok) {
std::ofstream out(*cpp_output);
if (out.fail()) {
std::cerr << "failed to create '" << *cpp_output << "'\n";
return 1;
}
auto mod = module_name_of_file(path.get_path(), mod_fn);
emit_cpp(out, env, mod, to_list(imports.begin(), imports.end()));
}