diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-17 09:51:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-17 09:51:19 +0000 |
| commit | b96cef1c1d86834ef6818f937b15cb6fd8bdb270 (patch) | |
| tree | 27f10b3f09239bfd00c4d65cabf6e897e37941a7 | |
| parent | 0ec22639868500d1b3a3755f64d6f002775530a8 (diff) | |
Patch by Dan Grayson to ensure that "Add LoadPath ... as ..." closes
the file descriptors on directories that it does not need to keep open
(the maximum number of simultaneously opened file descriptors
supported by the operating system is not so large in practice,
e.g. 256 on MacOS X).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14565 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | lib/system.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/system.ml b/lib/system.ml index fcead691a..edab24460 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -132,7 +132,7 @@ let canonical_path_name p = (* All subdirectories, recursively *) let exists_dir dir = - try let _ = opendir dir in true with Unix_error _ -> false + try let _ = closedir (opendir dir) in true with Unix_error _ -> false let skipped_dirnames = ref ["CVS"; "_darcs"] |