aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-09-12 19:25:53 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-09-12 19:25:53 +0000
commitf4c2950671c9db2fbe3870911d9b6034febd4b2c (patch)
tree42ef2311cb70cd7aeb57ce210bdb3d028660e409 /tools
parent30616eea6b706c36c2f28b92b9b8ba30009fcef6 (diff)
Message pour les erreurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4382 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rwxr-xr-xtools/coqdep.ml5
1 files changed, 1 insertions, 4 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 45353d7f9..c287dbbfd 100755
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -369,10 +369,7 @@ let all_subdirs root_dir log_dir =
let l = ref [(root_dir,[log_dir])] in
let add f = l := f :: !l in
let rec traverse phys_dir dir =
- let dirh =
- try opendir phys_dir
- with Unix_error _ -> invalid_arg "all_subdirs"
- in
+ let dirh = handle_unix_error opendir phys_dir in
try
while true do
let f = readdir dirh in