]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/helm_wget.in
Initial revision
[helm.git] / helm / interface / helm_wget.in
1 #!@PERL_BINARY@
2
3 if ($#ARGV != 1) {
4  print STDERR "Usage: helm_wget prefix URL\n";
5  exit -1;
6 }
7
8 my ($prefix,$URL) = @ARGV;
9 if ($URL =~ /^file:\//) {
10  $URL =~ s/^file:\///;
11  my $command = "mkdir -p $prefix ; cp $URL $prefix";
12  print "$command\n";
13  system($command) == 0
14   or die "\"$command\" error";
15 } else {
16  my $command = "wget -c -P $prefix $URL";
17  system($command) == 0
18   or die "\"$command\" error";
19 }