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

fix(shell/lean): crash when trying to read file without extension

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-28 14:17:30 -08:00
parent 53f486835e
commit d082fb7402
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/shell/lean.cpp
View file

@ -431,7 +431,7 @@ int main(int argc, char ** argv) {
bool has_hlean = (default_k == input_kind::HLean);
for (int i = optind; i < argc; i++) {
char const * ext = get_file_extension(argv[i]);
if (strcmp(ext, "lean") == 0) {
if (ext && strcmp(ext, "lean") == 0) {
has_lean = true;
if (has_hlean) {
std::cerr << ".hlean file cannot be mixed with .lean files\n";
@ -439,7 +439,7 @@ int main(int argc, char ** argv) {
}
if (default_k == input_kind::Unspecified)
default_k = input_kind::Lean;
} else if (strcmp(ext, "hlean") == 0) {
} else if (ext && strcmp(ext, "hlean") == 0) {
has_hlean = true;
if (has_lean) {
std::cerr << ".lean file cannot be mixed with .hlean files\n";