Fetch gap release data from GitHub rather than gap-system.org#72
Fetch gap release data from GitHub rather than gap-system.org#72Joseph-Edwards wants to merge 1 commit intogap-actions:mainfrom
Conversation
|
The failures in the windows jobs seem sporadic and network related |
|
This would also prevent server problems for the gap website impacting CI jobs (a few days ago I couldn't reach gap-system.org at all, and was redirected to a university error page instead). That may/would have impacted CI jobs as well, though I didn't run any myself during the downtime. I'm not sure doing a |
|
I'm slightly concerned about being rate limited too (though, admittedly, I have no real idea how often this action is used). An alternative would be to duplicate the |
The macOS runners using this action have recently started failing (see, for example, semigroups/Semigroups#1087 or https://github.com/Joseph-Edwards/setup-gap/actions/runs/21633236857/job/62351347716). This seems to be because
wget https://www.gap-system.org/releases.jsonis timing out after DNS succeeds but before an HTTPS connection can be established.I'm not entirely sure why this has started happening, but it seems like something is blocking the runner's access to gap-system.org.
This PR address this issue by replacing
https://www.gap-system.org/releases.jsonwith it's "source" filehttps://raw.githubusercontent.com/gap-system/GapWWW/master/releases.json.