From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 29 May 2006 14:12:40 +0000 (+0000)
Subject: bug fix: use an (un)marshaller for get_opt instead of a getter
X-Git-Tag: make_still_working~7309
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=43b1a4790cd6215742cfa0ab66ec01f3054a5a9c;p=helm.git

bug fix: use an (un)marshaller for get_opt instead of a getter
---

diff --git a/helm/software/components/getter/http_getter_env.ml b/helm/software/components/getter/http_getter_env.ml
index 79b0ab42e..af5896ea8 100644
--- a/helm/software/components/getter/http_getter_env.ml
+++ b/helm/software/components/getter/http_getter_env.ml
@@ -39,7 +39,7 @@ let prefix_RE = Pcre.regexp "^\\s*([^\\s]+)\\s+([^\\s]+)\\s*(.*)$"
 
 let cache_dir  = lazy (normalize_dir (Helm_registry.get "getter.cache_dir"))
 let dtd_dir = lazy (
-  match Helm_registry.get_opt Helm_registry.get_string "getter.dtd_dir" with
+  match Helm_registry.get_opt Helm_registry.string "getter.dtd_dir" with
   | None -> None
   | Some dir -> Some (normalize_dir dir))
 let dtd_base_urls  = lazy (