diff options
Diffstat (limited to 'lib/system.ml')
-rw-r--r-- | lib/system.ml | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/lib/system.ml b/lib/system.ml index 02d5e963f..2e35a98f7 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -79,12 +79,20 @@ let make_dir_table dir = Unix.closedir a; !b let exists_in_dir_respecting_case dir bf = - let contents = - try StrMap.find dir !dirmap with Not_found -> + let contents, cached = + try StrMap.find dir !dirmap, true with Not_found -> let contents = make_dir_table dir in dirmap := StrMap.add dir contents !dirmap; - contents in - StrSet.mem bf contents + contents, false in + StrSet.mem bf contents || + if cached then begin + (* rescan, there is a new file we don't know about *) + let contents = make_dir_table dir in + dirmap := StrMap.add dir contents !dirmap; + StrSet.mem bf contents + end + else + false let file_exists_respecting_case path f = (* This function ensures that a file with expected lowercase/uppercase |