X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fhttp_getter%2Fhttp_getter_misc.ml;h=880ddd46e4cb71060d28a2932e128d47b98b518a;hp=ab517e20ed66fdf57a188591b69e984d2ced1b10;hb=b077aa16b12755c2bace508154773efc9fa2320c;hpb=cf497123176d912bdef9baa16c25ace0ad9477fe

diff --git a/helm/http_getter/http_getter_misc.ml b/helm/http_getter/http_getter_misc.ml
index ab517e20e..880ddd46e 100644
--- a/helm/http_getter/http_getter_misc.ml
+++ b/helm/http_getter/http_getter_misc.ml
@@ -46,14 +46,34 @@ let hashtbl_sorted_fold f tbl init =
   in
   List.fold_left (fun acc k -> f k (Hashtbl.find tbl k) acc) init sorted_keys
 
-let wget ?output url =
-  let flags =
-    (match output with Some file -> ["-O"; file] | None -> []) @ [url]
-  in
-  debug_print ("wget " ^ String.concat " " flags);
+let cp src dst =
   Shell.call
     ~stdout:Shell.to_dev_null ~stderr:Shell.to_dev_null
-    [Shell.cmd "wget" flags]
+    [Shell.cmd "cp" [src; dst]]
+
+let file_scheme_RE = Pcre.regexp "^file://"
+let wget ?output url =
+  let use_wget () =
+    let flags =
+      (match output with Some file -> ["-O"; file] | None -> []) @ [url]
+    in
+    debug_print ("wget " ^ String.concat " " flags);
+    Shell.call
+      ~stdout:Shell.to_dev_null ~stderr:Shell.to_dev_null
+      [Shell.cmd "wget" flags]
+  in
+  if Pcre.pmatch ~rex:file_scheme_RE url then begin (* file:// URL *)
+    let src_fname = Pcre.replace ~rex:file_scheme_RE url in
+    match output with
+    | Some dst_fname -> cp src_fname dst_fname
+    | None ->
+        let dst_fname = Filename.basename src_fname in
+        if src_fname <> dst_fname then
+          cp src_fname dst_fname
+        else  (* src and dst are the same: do nothing *)
+          ()
+  end else  (* other URL, pass it to wget *)
+    use_wget ()
 
   (* stderr shown as usual *)
 let gzip ?(keep = false) fname =