Skip to content

Conversation

@tothtamas28
Copy link
Contributor

From commit 8db489b.

@tothtamas28 tothtamas28 self-assigned this Jan 14, 2026
@tothtamas28 tothtamas28 marked this pull request as ready for review January 14, 2026 12:01
@tothtamas28 tothtamas28 requested a review from Stevengre January 14, 2026 13:25
Copy link
Collaborator

@dkcumming dkcumming left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

@automergerpr-permission-manager automergerpr-permission-manager bot merged commit 9ff569b into master Jan 14, 2026
7 checks passed
@automergerpr-permission-manager automergerpr-permission-manager bot deleted the add-lemma branch January 14, 2026 15:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants