Automatically close issues and delete branches on PR merge

[larshinueber]

• 1. Update the branch protection rule for the standard main/develop branches so that they cannot be deleted by developers
• 2. Apply setting to automatically delete head branches after a PR has been merged to keep the branches clean (Settings -> General -> scroll down to Pull Requests -> tick "Automatically delete head branches")
• 3. Go through stale branches in repositories and delete them if no longer relevant

[larshinueber]

@HannoSpreeuw This was converted from a draft issue I created some time ago. Since you're already looking into the branch protection rules, the only relevant step would be step 2.

Additionally, to automatically close issues that are linked to a PR, we should make the develop branch our default branch (this was discussed before, please confirm @DominicDirkx), since only merging a PR to the repo default branch will close the issue (see https://docs.github.com/en/issues/tracking-your-work-with-issues/using-issues/linking-a-pull-request-to-an-issue#about-linked-issues-and-pull-requests).

[DominicDirkx]

Default branch changed to develop

[luigigisolfi]

Since this draft issue has been converted, should we close #609?

[larshinueber]

I would say that #609 is slightly different in scope, because it is about automatically removing closed PRs from the board, whereas this issue is about closing issues automatically once a PR has been merged to develop.

I would also extend #609 to automatically remove issues (and not only PRs) from the board once closed.

[HannoSpreeuw]

Okay, I ticked

Automatically delete head branches

in Settings --> General, under Pull Requests.