download.pl: add jsDelivr mirror for GitHub

This commit is contained in:
LEAN-ESX 2019-11-11 19:58:10 -08:00
parent 48387b3805
commit be770de958

View File

@ -203,9 +203,13 @@ foreach my $mirror (@ARGV) {
push @mirrors, "ftp://apache.cs.utah.edu/apache.org/$1";
push @mirrors, "ftp://apache.mirrors.ovh.net/ftp.apache.org/dist/$1";
} elsif ($mirror =~ /^\@GITHUB\/(.+)$/) {
my $dir = $1;
my $i = 0;
# replace the 2nd '/' with '@' for jsDelivr mirror
push @mirrors, "https://cdn.jsdelivr.net/gh/". $dir =~ s{\/}{++$i == 2 ? '@' : $&}ger;
# give github a few more tries (different mirrors)
for (1 .. 5) {
push @mirrors, "https://raw.githubusercontent.com/$1";
push @mirrors, "https://raw.githubusercontent.com/$dir";
}
} elsif ($mirror =~ /^\@GNU\/(.+)$/) {
push @mirrors, "https://mirror.csclub.uwaterloo.ca/gnu/$1";