Skip to content

Conversation

@nmattia
Copy link
Contributor

@nmattia nmattia commented Jan 30, 2026

The patch does not seem to be required anymore for the build to succeed.

The patch does not seem to be required anymore for the build to succeed.
@github-actions github-actions bot added the chore label Jan 30, 2026
@nmattia nmattia marked this pull request as ready for review January 30, 2026 15:38
@nmattia nmattia requested a review from a team as a code owner January 30, 2026 15:38
@nmattia nmattia enabled auto-merge January 30, 2026 15:38
@github-actions github-actions bot added the @idx label Jan 30, 2026
@nmattia nmattia added this pull request to the merge queue Jan 30, 2026
@nmattia nmattia removed this pull request from the merge queue due to a manual request Jan 30, 2026
@nmattia
Copy link
Contributor Author

nmattia commented Jan 30, 2026

Just to make sure I'll wait for #8602 to land first

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants