diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/system.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/lib/system.ml b/lib/system.ml index eec007dcab..a9db95318f 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -83,7 +83,9 @@ let file_exists_respecting_case path f = let rec aux f = let bf = Filename.basename f in let df = Filename.dirname f in - (String.equal df "." || aux df) + (* When [df] is the same as [f], it means that the root of the file system + has been reached. There is no point in looking further up. *) + (String.equal df "." || String.equal f df || aux df) && exists_in_dir_respecting_case (Filename.concat path df) bf in (!trust_file_cache || Sys.file_exists (Filename.concat path f)) && aux f |