Skip to content

Remove bors-ng and switch to GitHub actions merge-queue#480

Merged
lschuermann merged 1 commit intotock:masterfrom
lschuermann:dev/github-actions-mergequeue
Aug 1, 2023
Merged

Remove bors-ng and switch to GitHub actions merge-queue#480
lschuermann merged 1 commit intotock:masterfrom
lschuermann:dev/github-actions-mergequeue

Conversation

@lschuermann
Copy link
Copy Markdown
Member

This removes the bors configuration and switches to the GitHub actions merge queue merge bot. It replicates the required status checks for bors to pass, and adds the appropriate GitHub merge group status checks. This PR needs to be followed up with the appropriate configuration applied in the repository settings.

@lschuermann
Copy link
Copy Markdown
Member Author

In the interest of transparency, I made the following changes to this repository's configuration:

  • Created a branch protection rule for master, with the following settings:
    • Require a pull request before merging
      • Require approvals: at least 1 approval
      • Dismiss stale pull request approvals when new commits are pushed
    • Require status checks to pass before merging
      • Can't select any status checks as there have been no statuses pushed in the last week, will update, should be:
      • ci
      • size-diff
      • This replicates the bors.toml-required statuses

After this is merged, I will make the following further adjustments:

  • Select the required status as described above
  • Require the merge queue
    • Using merge commits
    • Only merging non-failing pull requests

@lschuermann
Copy link
Copy Markdown
Member Author

lschuermann commented Jul 31, 2023

Merging this with permission by @jrvanwhy in #476 (comment). However, CI is failing because of an update in elf2tab, fixing that by bumping the Rust toolchain version in #481 switching to the stable toolchain for elf2tab in #486.

This removes the bors configuration and switches to the GitHub actions
merge queue merge bot. It replicates the required status checks for
bors to pass, and adds the appropriate GitHub merge group status
checks. This PR needs to be followed up with the appropriate
configuration applied in the repository settings.
@lschuermann lschuermann force-pushed the dev/github-actions-mergequeue branch from abbf472 to ee10aac Compare August 1, 2023 17:24
@lschuermann lschuermann merged commit fd23ea2 into tock:master Aug 1, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants