diff options
| author | herbelin | 2011-10-17 09:51:19 +0000 |
|---|---|---|
| committer | herbelin | 2011-10-17 09:51:19 +0000 |
| commit | b96cef1c1d86834ef6818f937b15cb6fd8bdb270 (patch) | |
| tree | 27f10b3f09239bfd00c4d65cabf6e897e37941a7 /lib | |
| 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
Diffstat (limited to 'lib')
| -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 fcead691ac..edab244606 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"] |