Checking existance of things mentioned in documentation

Stream: mathlib4

[Daniel Weber]

It sometimes happens that when stuff is moved/renamed references to it in the documentation are missed, and broken links are created. Would it be possible to make CI to catch that?

[Yaël Dillies]

Is that not something we will get for free once we have switched to using Verso?

[Julian Berman]

That's basic functionality Sphinx has, so I'd suspect it's on the Verso radar (if it doesn't already solve it).

[Kim Morrison]

Yes, this is coming.