Skip to content

Conversation

@tgross35
Copy link
Contributor

@tgross35 tgross35 commented Dec 2, 2025

No description provided.

Copy link
Member

@marcoieni marcoieni left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I did the switch in the github settings

@marcoieni marcoieni enabled auto-merge December 3, 2025 15:02
@marcoieni marcoieni disabled auto-merge December 3, 2025 15:02
@bjorn3
Copy link
Member

bjorn3 commented Dec 3, 2025

Did you mean to disable automerge?

@marcoieni
Copy link
Member

yes, because the PR won't be merged anyway unless CI is green

@tgross35
Copy link
Contributor Author

tgross35 commented Dec 3, 2025

Timing, I wonder if rust-lang/rust#136795 may have regressed again

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