missing docstrings?

Stream: mathlib4

[Jared green]

im on lean 4.15.0, rev# 9837ca9d65d9de6fad1ef4381750ca688774e608.
i tried to import import Mathlib.Data.Lists.Sublists, Mathlib.Data.Multiset.Basic, Mathlib.Algebra.BigOperators.Group.List.Basic. in the infoview a get errors saying a bunch of definitions are missing a doc-string, the first one looks like this:
⚠ [24/474] Replayed Mathlib.Control.Combinators
warning: .\.\.lake/packages\mathlib\.\.\Mathlib\Control\Combinators.lean:35:4: Monad.mapM' is missing a doc-string, please add one.
Declarations whose name ends with a ' are expected to contain an explanation for the presence of a ' in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with set_option linter.docPrime false
any one of those imports triggers hundreds of errors just like that.

[Eric Wieser]

This was a bug in the linter's ignore mechanism, though I believe it doesn't hapen if you use lake exe cache get first

[Jared green]

nothing changes. do i also have to restart vs code?

[Jared green]

i had mistyped one of the imports.