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

I am happy to remove some nolints for you!
leanprover-community · Aug 13, 2021 · 3b37614 · 3b37614
1 parent 4a864ed
commit 3b37614
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt
@@ -39,7 +39,6 @@ src/data/array/lemmas.lean : line 9 : ERR_MOD : Module docstring missing, or too
 src/data/bitvec/basic.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 src/data/buffer/basic.lean : line 12 : ERR_MOD : Module docstring missing, or too late
 src/data/dlist/instances.lean : line 12 : ERR_MOD : Module docstring missing, or too late
-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/list/func.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/data/list/of_fn.lean : line 9 : ERR_MOD : Module docstring missing, or too late