aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/system.mli
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2015-09-18 12:12:05 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2015-09-20 00:14:32 +0200
commitb712864e9cf499f1298c1aca1ad8a8b17e145079 (patch)
tree7d4cc389b8f3de986dcea9414ebed559f6a36c30 /lib/system.mli
parentbfd0ee9503cf04b51b2dd40d4ad2a904b07ac323 (diff)
Revert "On MacOS X, ensuring that files found in the file system have the"
and "Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that files" and "Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on MacOS X." This reverts commits 4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606 and 69941d4e195650bf59285b897c14d6287defea0f and e7043eec55085f4101bfb126d8829de6f6086c5a. Trying to emulate a case sensitive file system on top of a case aware one is too costly: 3x slowdown when compiling the stdlib or CompCert.
Diffstat (limited to 'lib/system.mli')
-rw-r--r--lib/system.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/lib/system.mli b/lib/system.mli
index 051e92f16..a3d66d577 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -29,8 +29,6 @@ val exists_dir : string -> bool
val find_file_in_path :
?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
-val file_exists_respecting_case : string -> bool
-
(** {6 I/O functions } *)
(** Generic input and output functions, parameterized by a magic number
and a suffix. The intern functions raise the exception [Bad_magic_number]