From 0f3dd1243a236dc58ab64e7398024ff1d9d00afa Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 8 Nov 2018 09:52:26 +0000
Subject: Ensure termination of `file_exists_respecting_case`

---
 lib/system.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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
 
-- 
cgit v1.2.3