X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhttp_getter%2Fmain.ml;h=3117a85c991eed1be6c3cf81d14d2048cfe45683;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=e4cae512c8df2a810e357f68db6842b5e6f86601;hpb=faa5dd9616d34b5ceb30ad693dcfdc34479d4a5e;p=helm.git diff --git a/helm/http_getter/main.ml b/helm/http_getter/main.ml index e4cae512c..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