Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#4944)
Browse files Browse the repository at this point in the history
I am happy to remove some nolints for you!
  • Loading branch information
leanprover-community-bot committed Nov 8, 2020
1 parent e7d40ef commit 26e4f15
Showing 1 changed file with 14 additions and 14 deletions.
28 changes: 14 additions & 14 deletions scripts/copy-mod-doc-exceptions.txt
Expand Up @@ -427,20 +427,19 @@ src/category_theory/limits/over.lean : line 72 : ERR_LIN : Line has more than 10
src/category_theory/limits/over.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/pi.lean : line 58 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/pi.lean : line 88 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 104 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 111 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 249 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 257 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 261 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 299 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 306 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 382 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 101 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 121 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 128 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 269 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 277 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 298 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 336 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 343 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 474 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 67 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 72 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 76 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 82 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 84 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/shapes.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/preserves/basic.lean : line 99 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/binary_products.lean : line 243 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/binary_products.lean : line 343 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/binary_products.lean : line 348 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -475,7 +474,7 @@ src/category_theory/limits/shapes/constructions/over/products.lean : line 87 : E
src/category_theory/limits/shapes/constructions/preserve_binary_products.lean : line 63 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/constructions/pullbacks.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/shapes/equalizers.lean : line 33 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/equalizers.lean : line 734 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/equalizers.lean : line 775 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/finite_limits.lean : line 146 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/finite_limits.lean : line 149 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/finite_limits.lean : line 186 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1099,7 +1098,8 @@ src/geometry/manifold/times_cont_mdiff.lean : line 523 : ERR_LIN : Line has more
src/geometry/manifold/times_cont_mdiff.lean : line 900 : ERR_LIN : Line has more than 100 characters
src/group_theory/abelianization.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/group_theory/archimedean.lean : line 43 : ERR_LIN : Line has more than 100 characters
src/group_theory/coset.lean : line 251 : ERR_LIN : Line has more than 100 characters
src/group_theory/coset.lean : line 173 : ERR_LIN : Line has more than 100 characters
src/group_theory/coset.lean : line 260 : ERR_LIN : Line has more than 100 characters
src/group_theory/coset.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/group_theory/eckmann_hilton.lean : line 98 : ERR_LIN : Line has more than 100 characters
src/group_theory/free_abelian_group.lean : line 14 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -2024,7 +2024,7 @@ src/topology/sequences.lean : line 183 : ERR_LIN : Line has more than 100 charac
src/topology/sequences.lean : line 210 : ERR_LIN : Line has more than 100 characters
src/topology/sequences.lean : line 274 : ERR_LIN : Line has more than 100 characters
src/topology/sequences.lean : line 312 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/forget.lean : line 145 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/forget.lean : line 147 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/presheaf.lean : line 106 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/presheaf.lean : line 40 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/presheaf.lean : line 57 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit 26e4f15

Please sign in to comment.