issue !4#13328: Broken link in mathlib4_docs

Stream: triage

[Random Issue Bot]

Today I chose issue 13328 for discussion!

Broken link in mathlib4_docs
Created by @Florent Schaffhauser (@matematiflo) on 2024-05-29
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Kevin Buzzard]

Looks like it's still relevant, at least

[Ruben Van de Velde]

Looks like the issue now became that the tests don't get their documentation generated, which may be "won't fix"