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

I am happy to remove some nolints for you!
leanprover-community · May 7, 2021 · cd5864f · cd5864f
1 parent 6a7ddcc
commit cd5864f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt
@@ -17,7 +17,7 @@ src/category_theory/limits/creates.lean : line 329 : ERR_LIN : Line has more tha
 src/category_theory/limits/creates.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/category_theory/limits/functor_category.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/category_theory/limits/lattice.lean : line 9 : ERR_MOD : Module docstring missing, or too late
-src/category_theory/limits/opposites.lean : line 9 : ERR_MOD : Module docstring missing, or too late
+src/category_theory/limits/opposites.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/category_theory/limits/shapes/finite_products.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/category_theory/limits/shapes/products.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/category_theory/limits/types.lean : line 10 : ERR_MOD : Module docstring missing, or too late