gap-system/gap

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 and newest_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.
  • 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 is assets/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)