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 /dev | |
| 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 'dev')
0 files changed, 0 insertions, 0 deletions