X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhttp_getter%2Fmain.ml;h=3117a85c991eed1be6c3cf81d14d2048cfe45683;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=33ca1ffabfd8bccafe0c3be43b66c55421bd705a;hpb=76000efbc771b53f15a502d558a5b7b0297c9c6b;p=helm.git

diff --git a/helm/http_getter/main.ml b/helm/http_getter/main.ml
index 33ca1ffab..3117a85c9 100644
--- a/helm/http_getter/main.ml
+++ b/helm/http_getter/main.ml
@@ -271,13 +271,16 @@ let callback (req: Http_types.request) outchan =
     | "/help" -> return_help outchan
     | "/getxml" ->
         let uri = req#param "uri" in
-        let fname = Http_getter.getxml uri in
+        let fname = Http_getter.getxml uri in (* local name, in cache *)
+        let remote_name = Http_getter.resolve uri in (* remote name *)
         let src_enc = if is_gzip fname then `Gzipped else `Normal in
         let enc = parse_enc req in
         let fname, cleanup = convert_file ~from_enc:src_enc ~to_enc:enc fname in
         let contenc = if enc = `Gzipped then Some "x-gzip" else None in
         let patch_fun =
-          if parse_patch req then Some (patch_fun_for uri fname) else None
+          if parse_patch req
+          then Some (patch_fun_for uri remote_name)
+          else None
         in
         let gunzip = (enc = `Gzipped) in
         (try
@@ -315,17 +318,6 @@ let callback (req: Http_types.request) outchan =
   | Internal_error msg ->
       log_failure msg;
       return_html_internal_error ("internal_error", msg) msg outchan
-  | Shell.Subprocess_error l ->
-      let msgs =
-        List.map
-          (fun (cmd, code) ->
-            sprintf "Command '%s' returned %s" cmd (string_of_proc_status code))
-          l
-      in
-      let msg = String.concat ", " msgs in
-      log_failure msg;
-      return_html_internal_error ("subprocess_error", msg)
-        (String.concat "<br />\n" msgs) outchan
   | exn ->
       let msg = "uncaught exception: " ^ (Printexc.to_string exn) in
       (match exn with