Skip to content

Conversation

edwin0cheng
Copy link
Contributor

Related: #12260 (comment)

@Veykril
Copy link
Member

Veykril commented Aug 10, 2022

@bors r+

@bors
Copy link
Contributor

bors commented Aug 10, 2022

📌 Commit c47914c has been approved by Veykril

It is now in the queue for this repository.

@bors
Copy link
Contributor

bors commented Aug 10, 2022

⌛ Testing commit c47914c with merge d79d9e1...

@bors
Copy link
Contributor

bors commented Aug 10, 2022

☀️ Test successful - checks-actions
Approved by: Veykril
Pushing d79d9e1 to master...

@bors bors merged commit d79d9e1 into rust-lang:master Aug 10, 2022
@edwin0cheng edwin0cheng deleted the improve-ws branch August 11, 2022 07:55
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.

3 participants