Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR is a cherry-pick of PR #24553, which has gone through the beta-nomination and beta-acceptance process. (It just missed being part of the mass cherry-pick in #24708 because I had not yet reviewed it at that time.)
It should not be marked with the usual bors commands (i.e. no "r+" messages to at-bors); it instead will be merged manually after I had double checked that it builds locally.
(In fact, some local experimentation indicates sending even a "try" to at-bors could confuse github as to the mergability of the PR, see #24941 )