diff --git a/make_site.py b/make_site.py index c9c1b878c..e9676f84b 100755 --- a/make_site.py +++ b/make_site.py @@ -408,8 +408,9 @@ def download_N_theorems(kind: NTheorems) -> dict: except KeyError: print(f'Error: {thms} entry {id} refers to a nonexistent declaration {decl}') continue - # note: the `header-data.json` data file uses doc-relative links - header = decl_info.header.replace('href="./Mathlib/', 'href="./mathlib4_docs/Mathlib/') + # note: the `header-data.json` data file uses doc-relative links; + # rewrite all of them to point into the mathlib4_docs subdirectory + header = decl_info.header.replace('href="./', 'href="./mathlib4_docs/') doc_decls.append(DocDecl( name=decl, decl_header_html = header, diff --git a/templates/glossary.md b/templates/glossary.md index db3f581bf..7bf4016f0 100644 --- a/templates/glossary.md +++ b/templates/glossary.md @@ -373,7 +373,7 @@ Good `simp` lemmas guide the `simp` tactic towards reducing complex expressions A convention within [Mathlib](#Mathlib) for expressing propositions with multiple equivalent forms in a single conventional one. -Examples and further detail can be found on [the `simp` page](simp.html#simp-normal-form). +Examples and further detail can be found on [the `simp` page](extras/simp.html#simp-normal-form). ### syntax linter