Skip to content

Turn on mathlib linters#133

Merged
kbuzzard merged 1 commit intokbuzzard:mainfrom
YaelDillies:mathlib_linters
Mar 13, 2026
Merged

Turn on mathlib linters#133
kbuzzard merged 1 commit intokbuzzard:mainfrom
YaelDillies:mathlib_linters

Conversation

@YaelDillies
Copy link
Contributor

No description provided.

@kbuzzard
Copy link
Owner

Thanks a lot!

@kbuzzard kbuzzard merged commit a03af04 into kbuzzard:main Mar 13, 2026
2 checks passed
@YaelDillies YaelDillies deleted the mathlib_linters branch March 13, 2026 23:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants