mathlib3
fix(scripts/mk_nolint): fix error introduced by #2090
#2170

Merged

fix(scripts/mk_nolint): fix error introduced by #2090 #2170

gebner merged 1 commit into master from nolint-fix

fix(scripts/mk_nolint): fix error introduced by #2090

132bda1a

gebner merged 422f6400 into master 6 years ago

gebner deleted the nolint-fix branch 6 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Milestone

No milestone