Update `dev/releases/update_website.py` for new website
Closed this issue · 0 comments
We need to update dev/releases/update_website.py
in several ways:
-
it scans the removed directory
_Releases
to determine what the latest GAP release is. But we can just read_data/release.json
for that instead?- note the the script currently distinguish between
known_release
andnewest_release
so it can in theory add releases that are not the "latest" (say if we wanted to make a GAP 4.12.3 release today). This is not really necessary to support. So the code can be simplified in this regard.
- note the the script currently distinguish between
-
it creates a file
_Releases/{version}.html
like_Releases/4.13.1.html
-- I think this can just be deleted. -
_data/package-infos/{version_safe}.json
now isassets/package-infos.json
-
_Packages/
is gone
I think we can actually considerably simplify update_website.py
if instead of grabbing a list of all releases known to GitHub, we only ask for the release that is marked as "latest". And then possibly check whether it is greater than the release currently in the website (not sure we really need to do that, though)