mathlib3
[Merged by Bors] - chore(scripts): update nolints.txt
#19227

Closed

[Merged by Bors] - chore(scripts): update nolints.txt #19227

ghost wants to merge 1 commit into master from nolints

chore(scripts): update nolints.txt

94f9e0b1

bors changed the title ~~chore(scripts): update nolints.txt~~ [Merged by Bors] - chore(scripts): update nolints.txt 2 years ago

bors closed this 2 years ago

bors deleted the nolints branch 2 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Milestone

No milestone