Commit d0c5d20
chore(scripts): update nolints.json (leanprover-community#32859)
I am happy to remove some nolints for you!
[workflow run for this PR](https://github.com/leanprover-community/mathlib4/actions/runs/20199788622)
Co-authored-by: leanprover-community-bot <leanprover.community@gmail.com>1 parent 1825e17 commit d0c5d20
1 file changed
+0
-1
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
169 | 169 | | |
170 | 170 | | |
171 | 171 | | |
172 | | - | |
173 | 172 | | |
174 | 173 | | |
175 | 174 | | |
| |||
0 commit comments