Skip to content

Conversation

@TwoFX
Copy link
Member

@TwoFX TwoFX commented Oct 30, 2025

This PR fixes an incomplete docstring.

@TwoFX TwoFX added the changelog-no Do not include this PR in the release changelog label Oct 30, 2025
@TwoFX TwoFX enabled auto-merge October 30, 2025 15:45
@TwoFX TwoFX added this pull request to the merge queue Oct 30, 2025
Merged via the queue into leanprover:master with commit c0ad969 Oct 30, 2025
19 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-no Do not include this PR in the release changelog

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant