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

Commit

Permalink
chore(scripts): update nolints.txt (#18486)
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 Feb 23, 2023
1 parent 3dadefa commit 296726c
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion scripts/style-exceptions.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ src/control/traversable/derive.lean : line 11 : ERR_MOD : Module docstring missi
src/data/array/lemmas.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/bitvec/basic.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/buffer/basic.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/qpf/multivariate/basic.lean : line 73 : ERR_LIN : Line has more than 100 characters
src/data/qpf/multivariate/basic.lean : line 76 : ERR_LIN : Line has more than 100 characters
src/data/qpf/univariate/basic.lean : line 35 : ERR_LIN : Line has more than 100 characters
src/data/rbmap/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/rbmap/default.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Expand Down

0 comments on commit 296726c

Please sign in to comment.