Our current release procedure is:
- Cut a release branch from main.
- Make the release with
make release-x.
- Push the release commit and release tag to the remote.
- Make and merge a PR.
However, this does not work on Github, since Github's "rebase and merge" strategy results in commit hashes changing after the merge. In turn, this means that the release tag create on the release branch now points to a commit not on the main branch. At that point, we need to delete the existing tag and re-tag on main.
We should fix this procedure to either
- Don't create a tag on the release branch and manually require tagging on
main after merging.
- Prevent PRs from being merged from the web UI and instead require merges to be done via the
git CLI to ensure proper fast-forwarding.
Sources:
Our current release procedure is:
make release-x.However, this does not work on Github, since Github's "rebase and merge" strategy results in commit hashes changing after the merge. In turn, this means that the release tag create on the release branch now points to a commit not on the
mainbranch. At that point, we need to delete the existing tag and re-tag onmain.We should fix this procedure to either
mainafter merging.gitCLI to ensure proper fast-forwarding.Sources: