Skip to content

Commit

Permalink
doc: tweak documention of the longLine linter (#15458)
Browse files Browse the repository at this point in the history
  • Loading branch information
grunweg authored and bjoernkjoshanssen committed Sep 11, 2024
1 parent 0ba866d commit 9a2ea54
Showing 1 changed file with 3 additions and 2 deletions.
5 changes: 3 additions & 2 deletions Mathlib/Tactic/Linter/Lint.lean
Original file line number Diff line number Diff line change
Expand Up @@ -219,6 +219,8 @@ initialize addLinter cdotLinter

end CDotLinter

/-! # The "longLine linter" -/

/-- The "longLine" linter emits a warning on lines longer than 100 characters.
We allow lines containing URLs to be longer, though. -/
register_option linter.longLine : Bool := {
Expand All @@ -237,8 +239,7 @@ def longLineLinter : Linter where run := withSetOptionIn fun stx ↦ do
return
if (← MonadState.get).messages.hasErrors then
return
-- TODO: once per-project settings are available,
-- revert this hack to make it only apply on `Mathlib`
-- TODO: once mathlib's Lean version includes leanprover/lean4#4741, make this configurable
unless #[`Mathlib, `test, `Archive, `Counterexamples].contains (← getMainModule).getRoot do
return
-- The linter ignores the `#guard_msgs` command, in particular its doc-string.
Expand Down

0 comments on commit 9a2ea54

Please sign in to comment.