3 commits

Author	SHA1	Message	Date
Oliver Klee	f1b4faa9eb	[TASK] Use the GitHub command line tool for automerges (#793) ... This way, we do not need to rely on a 3rd-party GitHub action for this anymore.	2023-04-05 16:15:01 +02:00
dependabot[bot]	4cec3c0380	Bump peter-evans/enable-pull-request-automerge from 2 to 3 (#777) ... Bumps [peter-evans/enable-pull-request-automerge](https://github.com/peter-evans/enable-pull-request-automerge) from 2 to 3. - [Release notes](https://github.com/peter-evans/enable-pull-request-automerge/releases) - [Commits](https://github.com/peter-evans/enable-pull-request-automerge/compare/v2...v3) --- updated-dependencies: - dependency-name: peter-evans/enable-pull-request-automerge dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>	2023-03-24 06:02:02 +00:00
Oliver Klee	f89dcb0842	[TASK] Switch to using GitHub's own automerge feature (#758) ... Our current automerging CI task does not work reliably. So instead of using a GitHub Action that does the automerging itself, we are now using a GitHub Action that only triggers GitHub's own automerge feature (which works a lot more reliably).	2023-02-24 11:20:27 +01:00