Commit 2026-07-03 09:38 e62ffd55
View on Github →chore: fix bad indentation (#40853) Not exhaustive at all. Inspired by Zulip discussion in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/linter.20requests/with/605217189
chore: fix bad indentation (#40853) Not exhaustive at all. Inspired by Zulip discussion in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/linter.20requests/with/605217189