chore(scripts): update nolints.txt (#7902)

I am happy to remove some nolints for you!
leanprover-community · Jun 12, 2021 · 55c9662 · 55c9662
1 parent 2974a9f
commit 55c9662
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt
@@ -52,7 +52,6 @@ src/data/fintype/basic.lean : line 16 : ERR_MOD : Module docstring missing, or t
 src/data/fintype/sort.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/data/int/basic.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 src/data/int/cast.lean : line 9 : ERR_MOD : Module docstring missing, or too late
-src/data/int/modeq.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/data/int/range.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/data/int/sqrt.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/data/list/bag_inter.lean : line 8 : ERR_MOD : Module docstring missing, or too late