Documentation on lint overrides?

Stream: mathlib4

[Arien Malec]

Is there documentation on lint overrides?

I have a PR that needs to allow deprecated references & sorrys (because I'm porting to expose code that's deprecated to Std implementations), but don't know the magic invocations needed.

[Arien Malec]

Ping?

[Jireh Loreaux]

section
set_option linter.deprecated false

-- deprecated code

end

However, I highly doubt you are actually going to be allowed sorrys. Are you sure the approach you're taking regarding porting these is the right one?

[Arien Malec]

Thanks -- yes, was requested by @Mario Carneiro to preserve theorems to backport to Std4

[Mario Carneiro]

the sorrys are pending migration to Std. You should use this to placate CI:

-- FIXME: remove this when the sorries are gone
set_option warningAsError false