c3ab70cc98
Switch the release trigger from PR to a git tag. In practice this would mean tagging a commit in master branch and pushing it with `git push --tags`. The benefit of this is that tagging is already an event that is reserved for maintainers, so we can remove the need for verifying whether the event was done by a maintainer. We also no longer need to keep track of the tag. Previously the trigger was a PR which has a different ref from the tag, so manual bookkeeping was required to ensure github used the tag reference instead of the PR reference. Having the tagging itself be the trigger removes this need entirely as the default checkout will already use the tag as reference. |
||
|---|---|---|
| .. | ||
| build.yml | ||
| checks.yml | ||
| ci.yml | ||
| release.yml | ||
| sanitize.yml | ||