Zulip Chat Archive
Stream: mathlib4
Topic: Silent docstring linter
Yaël Dillies (Aug 27 2023 at 19:38):
In #2508, the docstring linter doesn't complain even though this definition doesn't have a docstring. Anybody know why?
Eric Wieser (Aug 27 2023 at 20:18):
The linter was recently enabled on master, but probably that PR hasn't merged master for a while?
Last updated: May 02 2025 at 03:31 UTC