From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 4 Feb 2005 15:03:58 +0000 (+0000)
Subject: bugfix: handling of local resources (not to be cached) when they are zipped,
X-Git-Tag: V_0_1_0~16
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e40f7aa785fbcee495a26e6700ed8b1de1f683d2;p=helm.git

bugfix: handling of local resources (not to be cached) when they are zipped,
avoid former Sys_error exception for not existent files
---

diff --git a/helm/ocaml/getter/http_getter_cache.ml b/helm/ocaml/getter/http_getter_cache.ml
index 2802f9926..62a009c0f 100644
--- a/helm/ocaml/getter/http_getter_cache.ml
+++ b/helm/ocaml/getter/http_getter_cache.ml
@@ -76,7 +76,8 @@ let is_in_cache basename =
 let respond_xml
   ?(via_http = true) ?(enc = `Normal) ?(patch = true) ~url ~uri outchan
   =
-  let local_resource = Http_getter_misc.is_local_url url in
+  let local_part = Http_getter_misc.local_url url in
+  let local_resource = local_part <> None in
   let resource_type = resource_type_of_url url in
   let extension = extension_of_resource_type resource_type in
   let downloadname =
@@ -167,6 +168,7 @@ let respond_xml
   let tmp_short_circuit = fill_cache () in
   threadSafe#doReader (lazy(
     assert (local_resource || is_in_cache basename);
+    let basename = match local_part with Some f -> f | None -> basename in
     let resource_type =
       if local_resource then
         resource_type