X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fextlib%2FhExtlib.ml;h=3ee270e4e00b42fd0b012a512b11a92feef48c82;hb=718eb06483ac76c4eb3160277c02598f298d0968;hp=53d8c74e878b4f511877116160a4a74661a29a29;hpb=f06968e452cca8782e822d98bec9007404abcbbe;p=helm.git

diff --git a/components/extlib/hExtlib.ml b/components/extlib/hExtlib.ml
index 53d8c74e8..3ee270e4e 100644
--- a/components/extlib/hExtlib.ml
+++ b/components/extlib/hExtlib.ml
@@ -425,14 +425,14 @@ let estimate_size x =
 let normalize_path s = 
   let s = Str.global_replace (Str.regexp "//") "/" s in
   let l = Str.split (Str.regexp "/") s in
-  let rec aux = function
-    | [] -> []
-    | he::".."::tl -> aux tl
-    | he::"."::tl -> aux (he::tl)
-    | he::tl -> he :: aux tl
+  let rec aux acc = function
+    | [] -> acc
+    | he::"."::tl -> aux acc (he::tl)
+    | he::".."::tl when he <> ".." -> aux [] (acc @ tl)
+    | he::tl -> aux (acc@[he]) tl
   in
   (if Str.string_match (Str.regexp "^/") s 0 then "/" else "") ^
-  String.concat "/" (aux l)
+  String.concat "/" (aux [] l)
   ^ (if Str.string_match (Str.regexp "/$") s 0 then "/" else "")
 ;;
 
@@ -444,7 +444,8 @@ let find_in paths path =
        try
          if (Unix.stat path).Unix.st_kind = Unix.S_REG then path
          else aux tl
-       with Unix.Unix_error _ -> aux tl
+       with Unix.Unix_error _ as exn -> 
+               aux tl
    in
    try
      aux paths