fix: rewrite all doc-relative links in header HTML, fix glossary link#802
Closed
fix: rewrite all doc-relative links in header HTML, fix glossary link#802
Conversation
The header HTML from header-data.json contains doc-relative links for all prefixes (Archive/, Init/, Batteries/, etc.), but only ./Mathlib/ links were being rewritten to ./mathlib4_docs/Mathlib/. This caused broken links on 100.html and 1000.html for declarations in Archive/, Init/, and Batteries/. Fix by rewriting all href="./" links to href="./mathlib4_docs/", matching the existing treatment of docs_link on line 417. Also fix a broken relative link in the glossary: simp.html should be extras/simp.html. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR fixes two broken link issues found by the dead link checker in #792:
make_site.pyonly rewriteshref="./Mathlib/"links fromheader-data.jsonto point intomathlib4_docs/, butheader-data.jsonalso contains links with./Archive/,./Init/,./Batteries/, and./foundational_types.htmlprefixes. These were left unrewritten, producing 133 broken links on the 100.html and 1000.html pages. Fix by rewriting allhref="./"tohref="./mathlib4_docs/".The glossary entry for
simp-normal form links tosimp.html#simp-normal-form, but the actual page is atextras/simp.html.🤖 Prepared with Claude Code