aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/system.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/system.ml')
-rw-r--r--lib/system.ml13
1 files changed, 13 insertions, 0 deletions
diff --git a/lib/system.ml b/lib/system.ml
index d1cdd8efc..6364035e1 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -53,6 +53,19 @@ let all_subdirs ~unix_path:root =
if exists_dir root then traverse root [];
List.rev !l
+let file_really_exists f =
+ if Coq_config.arch = "Darwin" then
+ (* ensure that the file exists with expected case on the
+ case-insensitive but case-preserving default MacOS file system *)
+ let rec aux f =
+ Printf.eprintf ".%!";
+ let bf = Filename.basename f in
+ let df = Filename.dirname f in
+ String.equal df "." || String.equal df "/" ||
+ aux df && Array.exists (String.equal bf) (Sys.readdir df)
+ in aux f
+ else Sys.file_exists f
+
let rec search paths test =
match paths with
| [] -> []