From 9484ab6a04783b9ee8539b6a564f2a3b83629ae8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 Aug 2014 09:04:03 -0700 Subject: [PATCH] fix(util/lean_path): if directory 'foo' does not contain 'default.lean', then we should also check whether the file 'foo.lean' exists or not, fixes #102 Signed-off-by: Leonardo de Moura --- src/util/lean_path.cpp | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp index b7cb8df2e..4c1a2bb0c 100644 --- a/src/util/lean_path.cpp +++ b/src/util/lean_path.cpp @@ -160,10 +160,7 @@ bool is_known_file_ext(std::string const & fname) { return is_lean_file(fname) || is_olean_file(fname) || is_lua_file(fname); } -optional check_file(std::string const & path, std::string const & fname, char const * ext = nullptr) { - std::string file = path + g_sep + fname; - if (is_directory(file.c_str())) - file += g_sep + g_default_file_name; +optional check_file_core(std::string file, char const * ext) { if (ext) file += ext; std::ifstream ifile(file); @@ -173,6 +170,16 @@ optional check_file(std::string const & path, std::string const & f return optional(); } +optional check_file(std::string const & path, std::string const & fname, char const * ext = nullptr) { + std::string file = path + g_sep + fname; + if (is_directory(file.c_str())) { + std::string default_file = file + g_sep + g_default_file_name; + if (auto r = check_file_core(default_file, ext)) + return r; + } + return check_file_core(file, ext); +} + std::string name_to_file(name const & fname) { return fname.to_string(g_sep_str.c_str()); }