From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 26 May 2004 15:37:45 +0000 (+0000)
Subject: bugfix in /ls: removed double trailing "/"
X-Git-Tag: pre_subst_in_kernel~80
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0cecccac856404634b2712fe672a6c746ed373b9;p=helm.git

bugfix in /ls: removed double trailing "/"
---

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index 83dbc0e8c..cf2ee593c 100644
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -394,10 +394,11 @@ let ls =
       "^([^.]*\\.[^.]*)((\\.body)|(\\.proof_tree)|(\\.types))?(\\.ann)?$"
   in
   let (types_RE, types_ann_RE, body_RE, body_ann_RE,
-       proof_tree_RE, proof_tree_ann_RE) =
+       proof_tree_RE, proof_tree_ann_RE, trailing_slash_RE) =
     (Pcre.regexp "\\.types$", Pcre.regexp "\\.types\\.ann$",
      Pcre.regexp "\\.body$", Pcre.regexp "\\.body\\.ann$",
-     Pcre.regexp "\\.proof_tree$", Pcre.regexp "\\.proof_tree\\.ann$")
+     Pcre.regexp "\\.proof_tree$", Pcre.regexp "\\.proof_tree\\.ann$",
+     Pcre.regexp "/$")
   in
   let (slash_RE, til_slash_RE, no_slashes_RE) =
     (Pcre.regexp "/", Pcre.regexp "^.*/", Pcre.regexp "^[^/]*$")
@@ -407,7 +408,7 @@ let ls =
       ls_remote regexp
     else begin
       let pat =
-        "^" ^ regexp
+        Pcre.replace ~rex:trailing_slash_RE ("^" ^ regexp)
 (*         (match lsuri with Cic p -> ("cic:" ^ p) | Theory p -> ("theory:" ^ p)) *)
       in
       let (dir_RE, obj_RE) =