Can't disable directory dependency linter?

Stream: mathlib4

[David Loeffler]

It seems we now have a linter that complains about imports between certain combinations of top-level directories. However, it seems to be difficult to turn it off (for development/testing purposes). If you add set_option linter.directoryDependency false anywhere after the imports, then it doesn't work; but if you add it before the imports at the top of the file, then you get complaints from the header style linter.

[Yaël Dillies]

The list of exceptions is hardcoded in docs#Mathlib.Linter.DirectoryDependency.overrideAllowedImportDirs

[David Loeffler]

Thanks Yael, but I'm not sure how that answers my question, which is "what's the simplest way to disable this linter locally for a single file".

[Yaël Dillies]

There is no way. You need to add a global exception