From fe1f3f54833936c2343c4a5de977b7858caf1ce5 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 30 Sep 2024 12:08:26 +0000 Subject: [PATCH] chore(Tactic/Linter): do not import `TextBased` linter (#17187) `Mathlib.Tactic.Linter.TextBased` is only used by the script `lake exe lint-style` and therefore does not to be imported by Mathlib. --- Mathlib/Tactic/Linter.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Tactic/Linter.lean b/Mathlib/Tactic/Linter.lean index e40a62f821d5a..e5c4da4423d3c 100644 --- a/Mathlib/Tactic/Linter.lean +++ b/Mathlib/Tactic/Linter.lean @@ -11,4 +11,3 @@ This file is ignored by `shake`: import Mathlib.Tactic.Linter.FlexibleLinter import Mathlib.Tactic.Linter.HaveLetLinter import Mathlib.Tactic.Linter.MinImports -import Mathlib.Tactic.Linter.TextBased