Closed DaniBodor closed 1 week ago
actually, could you hold off on reviewing this for the moment. There's one more thing I'd like to change.
This PR is now ready for review @psomhorst
@DaniBodor Have you tested this? You say the PR will automatically be closed when the PR is merged, but there is no 'merge PR' action, only a 'merge branches' action. I cannot find any documentation on this automatically closing the PR.
That's a good point. I suggest moving forward with either this branch (where the old close line could be changed to a mark as merged line) or with #338, but not both. Either way, we should probably create a fork and test that it works as intended.
Let me know which solution you prefer.
@psomhorst , I've removed the changes to the github release workflow from this PR, so now it is just some minor style changes.
EDIT: I repurposed this PR to do only the tidying up stuff, and the not-closing PRs on release part is now handled by #338
5d075b5: removed one step from the github release workflow that marks PRs as "closed". They should be automatically marked as "merged" in the preceeding job, when the PR is actually merged.