diff options
| author | Pierre-Marie Pédrot | 2016-01-29 17:27:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-01-29 18:03:50 +0100 |
| commit | 0b644da20c714b01565f88dffcfd51ea8f08314a (patch) | |
| tree | 5a63fe126f7ae1f5d0e9460234291dd3dd55a78b /tools/coq_makefile.ml | |
| parent | 4953a129858a231e64dec636a3bc15a54a0e771c (diff) | |
| parent | 22a2cc1897f0d9f568ebfb807673e84f6ada491a (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'tools/coq_makefile.ml')
| -rw-r--r-- | tools/coq_makefile.ml | 8 |
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 |
