aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-07-18 11:22:15 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-07-20 15:44:13 +0200
commite234f3ef8161f0b30c5189c629e856af04a66340 (patch)
tree73412bcbb008bf0575da9da2efc1da11451cd8bc /lib
parentad8bf70ccc61849cfb1ade20ce426ea2ec74aa0e (diff)
Windows: Sys.is_dir "foo/" always says no (so we strip trailing slash)
Diffstat (limited to 'lib')
-rw-r--r--lib/minisys.ml6
1 files changed, 5 insertions, 1 deletions
diff --git a/lib/minisys.ml b/lib/minisys.ml
index b4382a3fe..1ed017e48 100644
--- a/lib/minisys.ml
+++ b/lib/minisys.ml
@@ -44,7 +44,11 @@ let ok_dirname f =
(* Check directory can be opened *)
let exists_dir dir =
- try Sys.is_directory dir with Sys_error _ -> false
+ let rec strip_trailing_slash dir =
+ let len = String.length dir in
+ if len > 0 && (dir.[len-1] = '/' || dir.[len-1] = '\\')
+ then strip_trailing_slash (String.sub dir 0 (len-1)) else dir in
+ try Sys.is_directory (strip_trailing_slash dir) with Sys_error _ -> false
let apply_subdir f path name =
(* we avoid all files and subdirs starting by '.' (e.g. .svn) *)