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

[Merged by Bors] - chore(scripts): update nolints.txt #6354

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore(scripts): update nolints.txt #6354

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions scripts/style-exceptions.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -367,8 +367,8 @@ src/data/seq/computation.lean : line 11 : ERR_MOD : Module docstring missing, or
src/data/seq/parallel.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/data/seq/seq.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/seq/wseq.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/set/basic.lean : line 2337 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 884 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 2340 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 887 : ERR_LIN : Line has more than 100 characters
src/data/set/countable.lean : line 143 : ERR_LIN : Line has more than 100 characters
src/data/set/countable.lean : line 159 : ERR_LIN : Line has more than 100 characters
src/data/set/disjointed.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -852,5 +852,5 @@ src/topology/uniform_space/separation.lean : line 421 : ERR_LIN : Line has more
src/topology/uniform_space/separation.lean : line 423 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/uniform_convergence.lean : line 320 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/uniform_embedding.lean : line 348 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/uniform_embedding.lean : line 394 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/uniform_embedding.lean : line 401 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/uniform_embedding.lean : line 393 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/uniform_embedding.lean : line 400 : ERR_LIN : Line has more than 100 characters