[Merged by Bors] - fix(Linter.MinImports): remove unnecessary declarations #10483
Triggered via issue
November 5, 2024 12:57
mathlib-bors[bot]
Status
Skipped
Total duration
2s
Artifacts
–
bot_fix_style_comment.yaml
on: issue_comment
Fix style issues from lint
0s