From b96cef1c1d86834ef6818f937b15cb6fd8bdb270 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 17 Oct 2011 09:51:19 +0000
Subject: 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
---
 lib/system.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

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"]
 
-- 
cgit v1.2.3