review comments

lakefile.lean

@@ -62,9 +62,8 @@ package mathlib where
 ## Mathlib libraries
 -/
 
-target nolints_style (pkg) : System.FilePath :=
-  inputTextFile <| pkg.dir / "scripts" / "nolints-style.txt"
-
+/-- This file is read by syntax linters (Mathlib/Tactic/Linter/DocPrime.lean), and so must be
+registered as a target for that file to depend on. -/
 target no_lints_prime_decls (pkg) : System.FilePath :=
   inputTextFile <| pkg.dir / "scripts" / "no_lints_prime_decls.txt"
 
@@ -73,10 +72,9 @@ lean_lib Mathlib where
   leanOptions := mathlibLeanOptions
   -- Mathlib also enforces these linter options, which are not active by default.
   moreServerOptions := mathlibOnlyLinters
-  extraDepTargets := #[
-    `nolints_style,
-    `no_lints_prime_decls
-  ]
+  -- Any data file read by syntax linters in mathlib. Files read by standalone scripts do not need
+  -- to be listed here.
+  extraDepTargets := #[`no_lints_prime_decls]
 
 -- NB. When adding further libraries, check if they should be excluded from `getLeanLibs` in
 -- `scripts/mk_all.lean`.