Skip to content

Conversation

@Kobzol
Copy link
Member

@Kobzol Kobzol commented Oct 21, 2024

It shouldn't really be needed on this repo.

Accompanying PR: rust-lang/chalk#818

wg-traits also had bors merge rights for chalk, but that WG has been archived, so I don't think that we need to deal with it further.

It shouldn't really be needed on this repo.
@marcoieni
Copy link
Member

Merging because this PR only changes bots and CI. I'm coordinating with Kobzol to switch from bors to github merge queues 👍
Zulip thread here.

@marcoieni marcoieni merged commit bd8c29e into rust-lang:master Oct 22, 2024
@Kobzol Kobzol deleted the chalk-remove-bors branch October 22, 2024 07:26
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