Created attachment 212702 [details]
[patch] update SITE_GITHUB_CLOUD (cloud.github.com down)
Today it seems cloud.github.com is not available:
% host -t any cloud.github.com
cloud.github.com is an alias for d24z2fz21y4fag.cloudfront.net.
% host -t any d24z2fz21y4fag.cloudfront.net.
d24z2fz21y4fag.cloudfront.net has no ANY record
Any port that has GHC for the master site is failing to fetch.
There is some anecdotal evidence that it is deprecated:
However, I did not find an authoritative statement of that.
Nonetheless, github.com seems to work instead:
Maybe MASTER_SITE_GITHUB_CLOUD should be renamed to MASTER_SITE_GITHUB_DOWNLOADS.
"downloads" is an official name of a class of files described by the github REST API, so that name seems more fitting.
% curl 'https://api.github.com/repos/sodabrew/libsieve/downloads' | g _url
% Total % Received % Xferd Average Speed Time Time Time Current
Dload Upload Total Spent Left Speed
100 1237 100 1237 0 0 2593 0 --:--:-- --:--:-- --:--:-- 2593