diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 074c17886..03ee0b69d 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -18,6 +18,8 @@ add_test(lean_luahook2 ${CMAKE_CURRENT_BINARY_DIR}/lean -c 100 "${LEAN_SOURCE_DI add_test(lean_lua1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "--lua" "${LEAN_SOURCE_DIR}/../tests/lua/single.lua") add_test(lean_lua2 ${LEAN_SOURCE_DIR}/cmake/redirect.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "-u" "${LEAN_SOURCE_DIR}/../tests/lua/single.lua") add_test(lean_unknown_option ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z") +add_test(lean_unknown_file1 ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean") +add_test(lean_unknown_file2 ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lua") # LEAN EXAMPLES diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 41cad92c2..09854d938 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -158,6 +158,10 @@ int main(int argc, char ** argv) { } if (k == input_kind::Lean) { std::ifstream in(argv[i]); + if (in.bad() || in.fail()) { + std::cerr << "Failed to open file '" << argv[i] << "'\n"; + return 1; + } parser p(f, in, &S, false, false); if (!p()) ok = false;