]> matita.cs.unibo.it Git - helm.git/commitdiff
bugfix: handling of local resources (not to be cached) when they are zipped,
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 4 Feb 2005 15:03:58 +0000 (15:03 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 4 Feb 2005 15:03:58 +0000 (15:03 +0000)
avoid former Sys_error exception for not existent files

helm/ocaml/getter/http_getter_cache.ml

index 2802f9926fc847637985450bcd812c20e1df106b..62a009c0f954e5cc0ae5f1c8a2b58bdb604f6cf9 100644 (file)
@@ -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