Skip to content

Conversation

@lolbinarycat
Copy link
Contributor

@GuillaumeGomez
Copy link
Member

Nice, thanks!

@GuillaumeGomez GuillaumeGomez merged commit 91dedbd into rust-lang:master Apr 3, 2025
1 check passed
@lolbinarycat
Copy link
Contributor Author

I think this is the fastest I've ever had a PR merged, wow

@GuillaumeGomez
Copy link
Member

I have merge rights on this repository and I was doing something else on the computer so the stars were aligned for the super fast tracked merge. 😉

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