[Merged by Bors] - feat: weekly linting for successful grind?
#250333
Triggered via issue
April 12, 2026 01:59
mathlib-bors[bot]
Status
Skipped
Total duration
1s
Artifacts
–
maintainer_merge.yml
on: issue_comment
Ping maintainers on Zulip
0s