Skip to content

Commit f43eb0d

Browse files
committed
chore: fix MathlibTest/Header, hopefully
1 parent e89d51d commit f43eb0d

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

Mathlib/Tactic/Linter/DirectoryDependency.lean

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -166,7 +166,9 @@ We always allow imports of `Init`, `Lean`, `Std`, `Qq` and
166166
def allowedImportDirs : NamePrefixRel := .ofArray #[
167167
-- This is used to test the linter.
168168
(`MathlibTest.DirectoryDependencyLinter, `Mathlib.Lean),
169-
(`MathlibTest, `Mathlib.Lean),
169+
(`MathlibTest.Header, `Mathlib.Tactic),
170+
(`MathlibTest.Header, `Mathlib.Deprecated),
171+
(`MathlibTest.Header, `Lake),
170172

171173
(`Mathlib.Util, `Batteries),
172174
(`Mathlib.Util, `Mathlib.Lean),

0 commit comments

Comments
 (0)