From 2d38d687f9ff34cf168fab8b2555e747dcde97ad Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 9 Nov 2000 12:56:25 +0000
Subject: all_subdirs teste si son argument est un repertoire; sinon ne fait
 rien

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@829 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/system.ml | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

(limited to 'lib/system.ml')

diff --git a/lib/system.ml b/lib/system.ml
index fd7e93bd0a..a967ed191c 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -16,8 +16,7 @@ type load_path_entry = {
 type load_path = load_path_entry list
 
 let exists_dir dir =
-  try let _ = opendir dir in true
-  with Unix_error _ -> false
+  try let _ = opendir dir in true with Unix_error _ -> false
 
 let all_subdirs root =
   let l = ref [] in
@@ -25,9 +24,7 @@ let all_subdirs root =
     l := { directory = f; root_dir = root; relative_subdir = rel } :: !l 
   in
   let rec traverse dir rel =
-    let dirh = 
-      try opendir dir with Unix_error _ -> invalid_arg "all_subdirs" 
-    in
+    let dirh = opendir dir in
     try
       while true do
 	let f = readdir dirh in
@@ -42,7 +39,8 @@ let all_subdirs root =
     with End_of_file ->
       closedir dirh
   in
-  traverse root ""; List.rev !l
+  if exists_dir root then traverse root ""; 
+  List.rev !l
 
 let safe_getenv_def var def =
   try 
-- 
cgit v1.2.3