aboutsummaryrefslogtreecommitdiff
path: root/tools/coq_makefile.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-01-29 17:27:49 +0100
committerPierre-Marie Pédrot2016-01-29 18:03:50 +0100
commit0b644da20c714b01565f88dffcfd51ea8f08314a (patch)
tree5a63fe126f7ae1f5d0e9460234291dd3dd55a78b /tools/coq_makefile.ml
parent4953a129858a231e64dec636a3bc15a54a0e771c (diff)
parent22a2cc1897f0d9f568ebfb807673e84f6ada491a (diff)
Merge branch 'v8.5'
Diffstat (limited to 'tools/coq_makefile.ml')
-rw-r--r--tools/coq_makefile.ml8
1 files changed, 7 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index f9bff3ac99..147759f5fc 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -99,7 +99,13 @@ let string_prefix a b =
let is_prefix dir1 dir2 =
let l1 = String.length dir1 in
let l2 = String.length dir2 in
- dir1 = dir2 || (l1 < l2 && String.sub dir2 0 l1 = dir1 && dir2.[l1] = '/')
+ let sep = Filename.dir_sep in
+ if dir1 = dir2 then true
+ else if l1 + String.length sep <= l2 then
+ let dir1' = String.sub dir2 0 l1 in
+ let sep' = String.sub dir2 l1 (String.length sep) in
+ dir1' = dir1 && sep' = sep
+ else false
let physical_dir_of_logical_dir ldir =
let le = String.length ldir - 1 in