From 7c2045fe89bee49c3eaf04b92fd05e577174dcb9 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 17 May 2004 11:35:37 +0000 Subject: [PATCH] bugfix: remove trailing slashes from dtd_base_urls --- helm/ocaml/getter/http_getter_env.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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 -- 2.39.2