From ff24441cf5f5aaa9efb67d8bbc71b2e504a960d2 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 13 Dec 2000 12:01:28 +0000
Subject: [PATCH] Now mywget is used instead of wget. mywget is a wrapper for
 wget that recognizes also file:/... URLs.

---
 helm/interface/getter.ml |  4 ++--
 helm/interface/mywget    | 19 +++++++++++++++++++
 2 files changed, 21 insertions(+), 2 deletions(-)
 create mode 100755 helm/interface/mywget

diff --git a/helm/interface/getter.ml b/helm/interface/getter.ml
index d79409c89..d3da5a579 100644
--- a/helm/interface/getter.ml
+++ b/helm/interface/getter.ml
@@ -20,7 +20,7 @@ module MapOfStrings = Map.Make(OrderedStrings);;
 
 let read_index url =
  let module C = Configuration in
-  if Sys.command ("wget -c -P " ^ C.tmpdir ^ " " ^ url ^ "/\"" ^
+  if Sys.command ("./mywget " ^ C.tmpdir ^ " " ^ url ^ "/\"" ^
    C.indexname ^ "\"") <> 0
   then
    raise (ErrorGetting url) ;
@@ -108,7 +108,7 @@ let get_file uri =
     begin
      let url = url_of_uri uri in
       (*CSC: use -q for quiet mode *)
-      if Sys.command ("wget -c -P " ^ dir ^ " \"" ^ url ^"\"") <> 0
+      if Sys.command ("./mywget " ^ dir ^ " \"" ^ url ^"\"") <> 0
       then
        raise (ErrorGetting url) ;
     end ;
diff --git a/helm/interface/mywget b/helm/interface/mywget
new file mode 100755
index 000000000..c6f3205b7
--- /dev/null
+++ b/helm/interface/mywget
@@ -0,0 +1,19 @@
+#!/usr/bin/perl
+
+if ($#ARGV != 1) {
+ print STDERR "Usage: mywget prefix URL\n";
+ exit -1;
+}
+
+my ($prefix,$URL) = @ARGV;
+if ($URL =~ /^file:\//) {
+ $URL =~ s/^file:\///;
+ my $command = "mkdir -p $prefix ; cp $URL $prefix";
+ print "$command\n";
+ system($command) == 0
+  or die "\"$command\" error";
+} else {
+ my $command = "wget -c -P $prefix $URL";
+ system($command) == 0
+  or die "\"$command\" error";
+}
-- 
2.39.2