diff --git a/scripts/copy-mod-doc-exceptions.txt b/scripts/copy-mod-doc-exceptions.txt index 9b219db9d6e5f..1512fb9c5cbe5 100644 --- a/scripts/copy-mod-doc-exceptions.txt +++ b/scripts/copy-mod-doc-exceptions.txt @@ -1154,8 +1154,8 @@ src/linear_algebra/basis.lean : line 93 : ERR_LIN : Line has more than 100 chara src/linear_algebra/char_poly/coeff.lean : line 190 : ERR_LIN : Line has more than 100 characters src/linear_algebra/char_poly/coeff.lean : line 24 : ERR_LIN : Line has more than 100 characters src/linear_algebra/char_poly/coeff.lean : line 26 : ERR_LIN : Line has more than 100 characters -src/linear_algebra/determinant.lean : line 12 : ERR_MOD : Module docstring missing, or too late -src/linear_algebra/determinant.lean : line 257 : ERR_LIN : Line has more than 100 characters +src/linear_algebra/determinant.lean : line 13 : ERR_MOD : Module docstring missing, or too late +src/linear_algebra/determinant.lean : line 258 : ERR_LIN : Line has more than 100 characters src/linear_algebra/direct_sum/finsupp.lean : line 24 : ERR_LIN : Line has more than 100 characters src/linear_algebra/direct_sum/tensor_product.lean : line 9 : ERR_MOD : Module docstring missing, or too late src/linear_algebra/dual.lean : line 8 : ERR_MOD : Module docstring missing, or too late @@ -1389,13 +1389,11 @@ src/ring_theory/ideal/operations.lean : line 865 : ERR_LIN : Line has more than src/ring_theory/ideal/operations.lean : line 93 : ERR_LIN : Line has more than 100 characters src/ring_theory/ideal/operations.lean : line 95 : ERR_LIN : Line has more than 100 characters src/ring_theory/ideal/operations.lean : line 991 : ERR_LIN : Line has more than 100 characters -src/ring_theory/integral_closure.lean : line 116 : ERR_LIN : Line has more than 100 characters -src/ring_theory/integral_closure.lean : line 121 : ERR_LIN : Line has more than 100 characters -src/ring_theory/integral_closure.lean : line 197 : ERR_LIN : Line has more than 100 characters -src/ring_theory/integral_closure.lean : line 412 : ERR_LIN : Line has more than 100 characters -src/ring_theory/integral_closure.lean : line 413 : ERR_LIN : Line has more than 100 characters -src/ring_theory/integral_closure.lean : line 414 : ERR_LIN : Line has more than 100 characters -src/ring_theory/integral_closure.lean : line 505 : ERR_LIN : Line has more than 100 characters +src/ring_theory/integral_closure.lean : line 118 : ERR_LIN : Line has more than 100 characters +src/ring_theory/integral_closure.lean : line 123 : ERR_LIN : Line has more than 100 characters +src/ring_theory/integral_closure.lean : line 199 : ERR_LIN : Line has more than 100 characters +src/ring_theory/integral_closure.lean : line 444 : ERR_LIN : Line has more than 100 characters +src/ring_theory/integral_closure.lean : line 535 : ERR_LIN : Line has more than 100 characters src/ring_theory/integral_domain.lean : line 104 : ERR_LIN : Line has more than 100 characters src/ring_theory/integral_domain.lean : line 124 : ERR_LIN : Line has more than 100 characters src/ring_theory/integral_domain.lean : line 129 : ERR_LIN : Line has more than 100 characters @@ -1415,7 +1413,7 @@ src/ring_theory/jacobson_ideal.lean : line 87 : ERR_LIN : Line has more than 100 src/ring_theory/jacobson_ideal.lean : line 97 : ERR_LIN : Line has more than 100 characters src/ring_theory/localization.lean : line 1188 : ERR_LIN : Line has more than 100 characters src/ring_theory/localization.lean : line 1350 : ERR_LIN : Line has more than 100 characters -src/ring_theory/localization.lean : line 1528 : ERR_LIN : Line has more than 100 characters +src/ring_theory/localization.lean : line 1529 : ERR_LIN : Line has more than 100 characters src/ring_theory/localization.lean : line 870 : ERR_LIN : Line has more than 100 characters src/ring_theory/multiplicity.lean : line 10 : ERR_MOD : Module docstring missing, or too late src/ring_theory/multiplicity.lean : line 142 : ERR_LIN : Line has more than 100 characters