You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Right now, just looking at this repository it is not clear how things are updated for a releases. We should document this in the repository, even if it just means pointing to docs somewhere else.
Some specific ideas:
the README.md should talk about it
relevant is of course the dev/releases/update_website.py script in the gap repository, so mention it, and also its README
all generated files should have at their top a comment which indicates they are generated, should not be modified by hand, and ideally also how they were generated. E.g. "DO NOT EDIT THIS FILE MANUALLY. It was generated by the update_website.py script from the gap repository"
pointers at the relevant CI jobs might also be helpful
The text was updated successfully, but these errors were encountered:
If all goes well then the sync workflow will detect a new release and open a PR here. Then it can be merged. This leaves updating docs.gap-system.org and files.gap-system.org -- I just left a comment in #250 which discusses how this could then be triggered by merging that PR
Right now, just looking at this repository it is not clear how things are updated for a releases. We should document this in the repository, even if it just means pointing to docs somewhere else.
Some specific ideas:
dev/releases/update_website.py
script in the gap repository, so mention it, and also its READMEThe text was updated successfully, but these errors were encountered: