Commit 2026-09-19 13:56 54faafd4

View on Github →

chore(Linter/DirectoryDependency): move forbidden directories into a JSON file (#41938)

Estimated changes

Modified Mathlib/Tactic/Linter/DirectoryDependency.lean

added def Mathlib.Linter.DirectoryDependency.forbiddenDirsPath

modified def Mathlib.Linter.DirectoryDependency.forbiddenImportDirs

added def Mathlib.Linter.DirectoryDependency.mathlibRoots

modified def Mathlib.Linter.checkBlocklist

Modified scripts/README.md

Created scripts/forbiddenDirs.json