Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#4926)
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
leanprover-community-bot committed Nov 7, 2020
1 parent 8ba0dde commit c4e8d74
Showing 1 changed file with 33 additions and 33 deletions.
66 changes: 33 additions & 33 deletions scripts/copy-mod-doc-exceptions.txt
View file
Expand Up @@ -109,13 +109,13 @@ src/algebra/invertible.lean : line 216 : ERR_LIN : Line has more than 100 charac
src/algebra/invertible.lean : line 224 : ERR_LIN : Line has more than 100 characters
src/algebra/invertible.lean : line 233 : ERR_LIN : Line has more than 100 characters
src/algebra/invertible.lean : line 84 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 249 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 253 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 352 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 639 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 655 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 859 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 912 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 259 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 263 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 366 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 653 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 669 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 873 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 926 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/classical.lean : line 124 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/classical.lean : line 215 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/classical.lean : line 363 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -312,8 +312,8 @@ src/category_theory/adjunction/basic.lean : line 280 : ERR_LIN : Line has more t
src/category_theory/adjunction/basic.lean : line 298 : ERR_LIN : Line has more than 100 characters
src/category_theory/adjunction/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/category_theory/adjunction/fully_faithful.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/category_theory/adjunction/limits.lean : line 118 : ERR_LIN : Line has more than 100 characters
src/category_theory/adjunction/limits.lean : line 126 : ERR_LIN : Line has more than 100 characters
src/category_theory/adjunction/limits.lean : line 137 : ERR_LIN : Line has more than 100 characters
src/category_theory/adjunction/limits.lean : line 145 : ERR_LIN : Line has more than 100 characters
src/category_theory/adjunction/limits.lean : line 42 : ERR_LIN : Line has more than 100 characters
src/category_theory/adjunction/limits.lean : line 50 : ERR_LIN : Line has more than 100 characters
src/category_theory/adjunction/limits.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -403,38 +403,38 @@ src/category_theory/limits/functor_category.lean : line 115 : ERR_LIN : Line has
src/category_theory/limits/functor_category.lean : line 40 : ERR_LIN : Line has more than 100 characters
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/limits.lean : line 1062 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1085 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1093 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1114 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1156 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1419 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1424 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1470 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1504 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1523 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1525 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1567 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1611 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1679 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1061 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1084 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1092 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1113 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1155 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1418 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1423 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1469 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1503 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1522 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1524 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1566 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1610 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1678 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 233 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 425 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 578 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 788 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 828 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 413 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 566 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 776 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 827 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/opposites.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/over.lean : line 72 : ERR_LIN : Line has more than 100 characters
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 231 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 239 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 243 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 281 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 288 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 346 : 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 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
Expand Down

0 comments on commit c4e8d74

Please sign in to comment.