Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove bors.toml #25

Merged
merged 2 commits into from
Jan 10, 2024
Merged

Remove bors.toml #25

merged 2 commits into from
Jan 10, 2024

Conversation

obbardc
Copy link
Contributor

@obbardc obbardc commented Jan 10, 2024

The repository now uses github merge queues for pull requests. Remove outdated bors.toml file & rework the CI job into allgreen.

Fixes: #21

@obbardc obbardc requested a review from sjoerdsimons January 10, 2024 09:49
@sjoerdsimons
Copy link
Contributor

I've setup the merge queue now, keyed to bors; really we should with this commit also change the workflow to the typicall allgreen one we hvae in other projects ;)

@obbardc
Copy link
Contributor Author

obbardc commented Jan 10, 2024

oops, I forgot about that and will fix it ;-)

The repository now uses github merge queues for pull requests. Remove
outdated bors.toml file

Fixes: #21
Signed-off-by: Christopher Obbard <[email protected]>
Rework the bors job (which signifies overall workflow status) into a more
generic job named allgreen.

Signed-off-by: Christopher Obbard <[email protected]>
@obbardc obbardc force-pushed the wip/obbardc/remove-bors branch from e27084c to 79507f2 Compare January 10, 2024 13:41
@obbardc obbardc marked this pull request as ready for review January 10, 2024 13:41
@sjoerdsimons sjoerdsimons added this pull request to the merge queue Jan 10, 2024
Merged via the queue into main with commit 2272103 Jan 10, 2024
12 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

Successfully merging this pull request may close these issues.

Switch to GitHub merge queues
2 participants