From b1a5fe3686ecd5b03e5c7c2efd95716a8e5270ea Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 4 Nov 2015 22:22:17 +0100 Subject: Fix for case-insensitive path looking continued (#2554): Adding a second chance to dynamically regenerate the file system cache when a file is not found (suggested by Guillaume M.). --- lib/system.ml | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) (limited to 'lib/system.ml') 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 -- cgit v1.2.3