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 89fc79c8856596caed552d4be2ab04eea237ef23..a7fe6be91d14701a69e0a150b31488a370e9c870 100644 (file)
--- 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