Zulip Chat Archive
Stream: triage
Topic: issue !4#13328: Broken link in mathlib4_docs
Random Issue Bot (Jan 04 2025 at 14:11):
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 (Jan 04 2025 at 14:22):
Looks like it's still relevant, at least
Ruben Van de Velde (Jan 04 2025 at 17:37):
Looks like the issue now became that the tests don't get their documentation generated, which may be "won't fix"
Random Issue Bot (Jun 19 2025 at 14:09):
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?
Random Issue Bot (Sep 10 2025 at 14:12):
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?
Bryan Gin-ge Chen (Sep 10 2025 at 14:15):
Perhaps doc-gen4's link generation logic should skip links to files that won't have their documentation generated?
Random Issue Bot (Nov 22 2025 at 14:12):
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 (Nov 22 2025 at 23:35):
still broken
Last updated: Dec 20 2025 at 21:32 UTC