-
Notifications
You must be signed in to change notification settings - Fork 163
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Teach "make bootstrap" to use curl
if wget
is not available
#1866
Comments
Would be great to get this into 4.9. Shouldn't be too hard either. E.g. we could add an #/bin/sh
set -e
command -v wget >/dev/null 2>&1 && exec wget "$@"
command -v curl >/dev/null 2>&1 && exec curl -O "$@"
echo "Error, failed to download: neither wget nor curl available"
exit 1 Then change Caveat: This disables a trick we use to make our Travis builds a bit more robust, by passing lots of extra options to wget in
It should still be possible to get this "robust" variant. Easiest would be to just add those options into Another option would be to simply replace |
As @alex-konovalov correctly pointed out to me, end users won't care about these targets, so no need to get this into 4.9 (won't hurt either, of course). |
Put this under GAP 4.10 milestone to help @cdwensley |
On macOS,
curl
is available butwget
is not.The text was updated successfully, but these errors were encountered: