Add bors

[matthiasbeyer]

This adds bors.

---

What you'd need to do: Go to https://bors.tech, add this repository (if you haven't done yet) and ensure the settings from this comment.

[matthiasbeyer]

There might be still an issue with the worflow file, as actions should already be triggered by this PR.

[philippkeller]

@matthiasbeyer I just added bors through https://github.com/apps/bors/installations/new - is there something more I need to do?

[matthiasbeyer]

Lets see whether bors knows of this repository... 😉

bors ping

[bors]

pong

[matthiasbeyer]

Nice. So yes, you'd need to ensure the settings I listed in this comment!

[philippkeller]

• Disable squash merges (not required for bors per se, but anyways a good option) ✅
• With "Require a pull request before merging" ✅
• With "Require status checks to pass before merging" ✅
• With "bors" as only required status check -> waiting until you configured bors
• "Require pull request reviews before merging" MUST be unmarked -> didn't find this setting, is it called "Require review from Code Owners" ?
• Required for administrators as well ✅

[matthiasbeyer]

Awesome.

So lets see whether bors can merge this. I doubt it right now, as actions seems not to run yet. I had this problem before, and I know how to resolve it. Give me a few minutes!

bors merge

[bors]

Build succeeded:

• CI

[matthiasbeyer]

I messed this up a bit. Bors already merged it.

[matthiasbeyer]

"Require pull request reviews before merging" MUST be unmarked -> didn't find this setting, is it called "Require review from Code Owners" ?

Yes, I think so.