Eric Wieser

#30 makes this work on repository pages as well

(I think this has been reported on Zulip before, but I couldn't find a tracking issue)

> PS: `M₂` is not a valid LaTeX formula; it should be `M_2`. Mathjax is quite happy to render $M₂$, though it admittedly looks worse than $M_2$

> So I think before feeding the docstring to markdown processor, we need to filter all LaTeX formulas This is not a sensible approach; the markdown parser needs to natively...

The prose itself isn't really what matters here; it's primarily about being able to ask "what instances does mathlib put on pi types", which is very much directly related to...

I think it's broken that way due to use of relative URLs in iframes. If you use absolute urls the issue should go away.

I don't think you can solve that. When generating the HTML for the 404 page I think the user needs to specify the folder that the site is hosted from....

> The reason for this relative linking is that doc-gen's pages are supposed to be hostable behind arbitrary prefixes without requiring any intervention from the user. I think the thing...

> 2\. But it does not perform a redirect to 404.html This is a feature; performing a redirect would amount to serving up a 30x status code, which would not...

The PR description should be a coherent summary, not a list of commit messages. If the commit messages are largely separate, then this should be separate PRs; for instance, perhaps...