gh-118401: Docs: Use Sphinx short options #118403
Merged
+1
−1
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.
On PRs which haven't synced with
main
yet, they're still installing Sphinx 7.2 instead of 7.3. That's fine.But when the CI runs, GitHub is using the workflow from
main
that has the 7.3-only long options, and not the workflow from their own branch that has the 7.2-and-7.3 short options. This is surprising.Quick fix: they can update their PR branches with
main
, but this will be disruptive for more PRs.Better fix: keep short options in the workflow for longer, perhaps until we upgrade Sphinx to 7.4 or 8.0.