Miscellaneous fixes #7173
Merged
Miscellaneous fixes #7173
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
8d420ec to
e0d0ab2
Compare
radoering
reviewed
Dec 11, 2022
radoering
reviewed
Dec 11, 2022
df7b63f to
53053d1
Compare
radoering
reviewed
Dec 11, 2022
80efe17 to
2e3043b
Compare
radoering
reviewed
Dec 15, 2022
04c9a5b to
96ead89
Compare
radoering
approved these changes
Dec 18, 2022
|
This pull request has been automatically locked since there has not been any recent activity after it was closed. Please open a new issue for related bugs. |
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
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.
A small collection of miscellaneous fixes, none of which have individually seemed to me worth the bother of a pull request. But I've now got enough of them queued up that, well, here we are.
Hopefully the commits and their messages are self-explanatory, these are all intended as uncontroversial. But if some of them are for some reason harder to merge than others then say so and this can be broken up into more PRs.