Skip to content

Conversation

@mdboom
Copy link
Contributor

@mdboom mdboom commented Dec 18, 2025

No description provided.

@mdboom mdboom requested a review from cpcloud December 18, 2025 17:21
@copy-pr-bot
Copy link
Contributor

copy-pr-bot bot commented Dec 18, 2025

Auto-sync is disabled for ready for review pull requests in this repository. Workflows must be run manually.

Contributors can view more details about this message here.

@leofang leofang merged commit 62a8cb3 into main Dec 18, 2025
1 check passed
@leofang leofang deleted the mdboom-patch-1 branch December 18, 2025 17:24
@leofang leofang added the to-be-backported Trigger the bot to raise a backport PR upon merge label Dec 18, 2025
@github-actions
Copy link

Backport failed for 12.9.x, because it was unable to cherry-pick the commit(s).

Please cherry-pick the changes locally and resolve any conflicts.

git fetch origin 12.9.x
git worktree add -d .worktree/backport-1408-to-12.9.x origin/12.9.x
cd .worktree/backport-1408-to-12.9.x
git switch --create backport-1408-to-12.9.x
git cherry-pick -x 62a8cb35c2d8110207ebe7e0e3926632fe6a31c1

@github-actions
Copy link

Doc Preview CI
Preview removed because the pull request was closed or merged.

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

Labels

to-be-backported Trigger the bot to raise a backport PR upon merge

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants