Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 6eb334b

Browse files
chore(scripts): update nolints.txt (#17777)
I am happy to remove some nolints for you!
1 parent 94825b2 commit 6eb334b

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

scripts/style-exceptions.txt

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ src/control/monad/cont.lean : line 13 : ERR_MOD : Module docstring missing, or t
33
src/control/monad/writer.lean : line 11 : ERR_MOD : Module docstring missing, or too late
44
src/control/traversable/derive.lean : line 11 : ERR_MOD : Module docstring missing, or too late
55
src/data/array/lemmas.lean : line 9 : ERR_MOD : Module docstring missing, or too late
6-
src/data/bitvec/basic.lean : line 10 : ERR_MOD : Module docstring missing, or too late
6+
src/data/bitvec/basic.lean : line 11 : ERR_MOD : Module docstring missing, or too late
77
src/data/buffer/basic.lean : line 11 : ERR_MOD : Module docstring missing, or too late
88
src/data/qpf/multivariate/basic.lean : line 73 : ERR_LIN : Line has more than 100 characters
99
src/data/qpf/univariate/basic.lean : line 35 : ERR_LIN : Line has more than 100 characters

0 commit comments

Comments
 (0)