[Merged by Bors] - chore(scripts): update nolints.json#32859
Closed
leanprover-community-bot-assistant wants to merge 1 commit intomasterfrom
Closed
[Merged by Bors] - chore(scripts): update nolints.json#32859leanprover-community-bot-assistant wants to merge 1 commit intomasterfrom
leanprover-community-bot-assistant wants to merge 1 commit intomasterfrom
Commits
Commits on Dec 14, 2025
- authored andcommitted
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?v=4&size=32){kind=avatar}