mathlib3

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

#2170

Merged