From d45da2d5ba9ee2b51d6ec5c63ccacfb810f4311f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Mar 2019 12:44:00 -0700 Subject: [PATCH] fix(shell/lean): check whether output file was created or not --- src/shell/lean.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index f3e86d773f..a8b4daa172 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -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())); }