From 1ba4c045833569b30fd61616aae739ecb7117ab8 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Thu, 1 Sep 2011 09:50:59 +0000
Subject: [/]+ is equivalent to [/] in System and its copy

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14435 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/system.ml | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

(limited to 'lib')

diff --git a/lib/system.ml b/lib/system.ml
index 5bd2df9957..fcead691ac 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -95,16 +95,26 @@ let lpath_from_path path path_separator =
 let rec remove_path_dot p =
   let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
   let n = String.length curdir in
-  if String.length p > n && String.sub p 0 n = curdir then
-    remove_path_dot (String.sub p n (String.length p - n))
+  let l = String.length p in
+  if l > n && String.sub p 0 n = curdir then
+    let n' =
+      let sl = String.length Filename.dir_sep in
+      let i = ref n in
+	while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in
+    remove_path_dot (String.sub p n' (l - n'))
   else
     p
 
 let strip_path p =
   let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *)
   let n = String.length cwd in
-  if String.length p > n && String.sub p 0 n = cwd then
-    remove_path_dot (String.sub p n (String.length p - n))
+  let l = String.length p in
+  if l > n && String.sub p 0 n = cwd then
+    let n' =
+      let sl = String.length Filename.dir_sep in
+      let i = ref n in
+	while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in
+    remove_path_dot (String.sub p n' (l - n'))
   else
     remove_path_dot p
 
-- 
cgit v1.2.3