Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5816)
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 Jan 20, 2021
1 parent d7a8709 commit b1d5673
Showing 1 changed file with 17 additions and 17 deletions.
34 changes: 17 additions & 17 deletions scripts/style-exceptions.txt
View file
Expand Up @@ -102,12 +102,12 @@ src/analysis/normed_space/bounded_linear_maps.lean : line 392 : ERR_LIN : Line h
src/analysis/normed_space/bounded_linear_maps.lean : line 447 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/finite_dimension.lean : line 177 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/finite_dimension.lean : line 290 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 1027 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 726 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 898 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 238 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 1005 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 704 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 876 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 234 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 34 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 649 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 645 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 91 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/arsinh.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/analysis/special_functions/pow.lean : line 1389 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -966,14 +966,14 @@ src/order/filter/bases.lean : line 259 : ERR_LIN : Line has more than 100 charac
src/order/filter/bases.lean : line 40 : ERR_LIN : Line has more than 100 characters
src/order/filter/bases.lean : line 625 : ERR_LIN : Line has more than 100 characters
src/order/filter/bases.lean : line 86 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1379 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1519 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1525 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1542 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1828 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1980 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 2113 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 2358 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1383 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1523 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1529 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1546 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1832 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1984 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 2117 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 2362 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 675 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 685 : ERR_LIN : Line has more than 100 characters
src/order/filter/extr.lean : line 301 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1490,9 +1490,9 @@ src/topology/local_extr.lean : line 267 : ERR_LIN : Line has more than 100 chara
src/topology/local_homeomorph.lean : line 508 : ERR_LIN : Line has more than 100 characters
src/topology/local_homeomorph.lean : line 519 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 109 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 1321 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 1327 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 15 : ERR_MOD : Module docstring missing, or too late
src/topology/metric_space/basic.lean : line 1684 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 1690 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 332 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 450 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 788 : ERR_LIN : Line has more than 100 characters
Expand All @@ -1505,8 +1505,8 @@ src/topology/metric_space/closeds.lean : line 265 : ERR_LIN : Line has more than
src/topology/metric_space/emetric_space.lean : line 19 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/emetric_space.lean : line 318 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/emetric_space.lean : line 36 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/emetric_space.lean : line 757 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/emetric_space.lean : line 767 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/emetric_space.lean : line 760 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/emetric_space.lean : line 770 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/emetric_space.lean : line 93 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/gromov_hausdorff.lean : line 61 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/gromov_hausdorff_realized.lean : line 103 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit b1d5673

Please sign in to comment.