diff --git a/Makefile.rules b/Makefile.rules index d25997f6ca..c0b9a5ad89 100644 --- a/Makefile.rules +++ b/Makefile.rules @@ -1105,13 +1105,13 @@ PKG_BRANCH = master PKG_BOOTSTRAP_URL = https://www.gap-system.org/pub/gap/gap4pkgs/ PKG_MINIMAL = packages-required-$(PKG_BRANCH).tar.gz PKG_FULL = packages-$(PKG_BRANCH).tar.gz -WGET = wget -N +DOWNLOAD = $(abs_srcdir)/etc/download.sh bootstrap-pkg-minimal: @if test -e pkg; then \ echo "The pkg directory already exists. Please move or remove it to proceed."; \ else \ - $(WGET) $(PKG_BOOTSTRAP_URL)$(PKG_MINIMAL) && \ + $(DOWNLOAD) $(PKG_BOOTSTRAP_URL)$(PKG_MINIMAL) && \ mkdir pkg && \ cd pkg && \ tar xzf ../$(PKG_MINIMAL) ; \ @@ -1121,7 +1121,7 @@ bootstrap-pkg-full: @if test -e pkg; then \ echo "The pkg directory already exists. Please move or remove it to proceed" ; \ else \ - $(WGET) $(PKG_BOOTSTRAP_URL)$(PKG_FULL) && \ + $(DOWNLOAD) $(PKG_BOOTSTRAP_URL)$(PKG_FULL) && \ mkdir pkg && \ cd pkg && \ tar xzf ../$(PKG_FULL) ; \ diff --git a/etc/ci-prepare.sh b/etc/ci-prepare.sh index a706809c77..00a8a49ac7 100644 --- a/etc/ci-prepare.sh +++ b/etc/ci-prepare.sh @@ -46,15 +46,15 @@ time make V=1 -j4 # download packages; instruct wget to retry several times if the # connection is refused, to work around intermittent failures -WGET="wget -N --no-check-certificate --tries=5 --waitretry=5 --retry-connrefused" +WGET="wget --tries=5 --waitretry=5 --retry-connrefused" if [[ $(uname) == Darwin ]] then # Travis OSX builders seem to have very small download bandwidth, # so as a workaround, we only test the minimal set of packages there. # On the upside, it's good to test that, too! - make bootstrap-pkg-minimal WGET="$WGET" + make bootstrap-pkg-minimal DOWNLOAD="$WGET" else - make bootstrap-pkg-full WGET="$WGET" + make bootstrap-pkg-full DOWNLOAD="$WGET" fi # check that GAP is at least able to start diff --git a/etc/download.sh b/etc/download.sh new file mode 100755 index 0000000000..2bbfbb7c06 --- /dev/null +++ b/etc/download.sh @@ -0,0 +1,16 @@ +#/bin/sh +# +# This script expects a single argument, which should be an URL pointing to a +# file for download; it then tries to download that file, into a local file +# with the same name as the remote file. +set -e + +# check whether curl is available, and if so, delegate to it +command -v curl >/dev/null 2>&1 && exec curl -O "$@" + +# check whether wget is available, and if so, delegate to it +command -v wget >/dev/null 2>&1 && exec wget -N "$@" + +# if no supported download tool is available, abort +echo "Error, failed to download: neither wget nor curl available" +exit 1