]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/helm_wget.in
mywget renamed in helm_wget; autoconf used for helm_wget
[helm.git] / helm / interface / helm_wget.in
diff --git a/helm/interface/helm_wget.in b/helm/interface/helm_wget.in
new file mode 100755 (executable)
index 0000000..b0d29df
--- /dev/null
@@ -0,0 +1,19 @@
+#!@PERL_BINARY@
+
+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";
+}