diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-05-15 17:42:16 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-05-15 18:04:08 +0200 |
commit | 4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606 (patch) | |
tree | bbc3aa63ec0ee105a1b7e88ddbcf052cd8c738b6 /lib | |
parent | 15dc0ff339e01341e11c5dec63689ddc3e500e96 (diff) |
On MacOS X, ensuring that files found in the file system have the
expected lowercase/uppercase spelling (based on a patch by Pierre B.).
This should fix #2554 (and see also discussion on coq-club, May 2015).
Diffstat (limited to 'lib')
-rw-r--r-- | lib/system.ml | 13 |
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 | [] -> [] |