aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-12 00:48:25 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-12 00:48:25 +0200
commitc5de2c3a2aa96c468e7583577141a93e359a9baf (patch)
treeba7283c2f1c25590fe95c7a57ba24e8ea80e7e7f /lib
parentaa6a7fc837f8148655c179e9a0b63c3044edfe71 (diff)
Fix bug #4722: Coq dies when encountering broken symbolic links.
Diffstat (limited to 'lib')
-rw-r--r--lib/system.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/system.ml b/lib/system.ml
index 205a5506c..b4b3882d3 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -35,7 +35,7 @@ let all_subdirs ~unix_path:root =
Array.iter (fun f ->
if ok_dirname f then
let file = Filename.concat dir f in
- if Sys.is_directory file then begin
+ if exists_dir file then begin
let newrel = rel @ [f] in
add file newrel;
traverse file newrel