From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 17 May 2004 11:35:37 +0000 (+0000)
Subject: bugfix: remove trailing slashes from dtd_base_urls
X-Git-Tag: V_0_0_9~52
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=7c2045fe89bee49c3eaf04b92fd05e577174dcb9

bugfix: remove trailing slashes from dtd_base_urls
---

diff --git a/helm/ocaml/getter/http_getter_env.ml b/helm/ocaml/getter/http_getter_env.ml
index 89fc79c88..a7fe6be91 100644
--- a/helm/ocaml/getter/http_getter_env.ml
+++ b/helm/ocaml/getter/http_getter_env.ml
@@ -47,8 +47,10 @@ let cic_dir         = lazy (Helm_registry.get "getter.cic_dir")
 let nuprl_dir       = lazy (Helm_registry.get "getter.nuprl_dir")
 let rdf_dir         = lazy (Helm_registry.get "getter.rdf_dir")
 let dtd_dir         = lazy (Helm_registry.get "getter.dtd_dir")
-let dtd_base_urls   = lazy (Helm_registry.get_string_list
-                              "getter.dtd_base_urls")
+let dtd_base_urls   = lazy (
+  let rex = Pcre.regexp "/*$" in
+  let raw_urls = Helm_registry.get_string_list "getter.dtd_base_urls" in
+  List.map (Pcre.replace ~rex) raw_urls)
 let port            = lazy (Helm_registry.get_int "getter.port")
 
 let _servers = ref None