Def Mathlib.Linter.DirectoryDependency.forbiddenDirsPath

Modification history

2026-10-21 00:36
Mathlib/Tactic/Linter/DirectoryDependency.lean
feat(Tactic/Linter/Header): access library root without cwd (#45061) …
Modified Mathlib.Linter.DirectoryDependency.forbiddenDirsPathView on Github →
2026-09-19 13:56
Mathlib/Tactic/Linter/DirectoryDependency.lean
chore(Linter/DirectoryDependency): move forbidden directories into a JSON file (#41938)
Added Mathlib.Linter.DirectoryDependency.forbiddenDirsPathView on Github →