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

@tgross35 tgross35 force-pushed the default-branch-name branch from fe881ae to 936db7f Compare December 5, 2025 02:35
@rustbot
Copy link
Collaborator

rustbot commented Dec 5, 2025

This PR was rebased onto a different main commit. Here's a range-diff highlighting what actually changed.

Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers.

@tgross35 tgross35 merged commit 936db7f into rust-lang:main Dec 5, 2025
38 checks passed
@tgross35 tgross35 deleted the default-branch-name branch December 5, 2025 02:50
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.

4 participants