Weird font in infoview

[abentkamp]

From Zulip: ~~https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/A.20set.20that.20must.20be.20a.20singletoneral.20times.2E~~

updated Link: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20A.20set.20that.20must.20be.20a.20singleton

This user has a weird font issue in the infoview:

Maybe this happens when the font "Source Code Pro" is not installed? This might be the user's default monospace font? We should probably ship the font with the website to make sure it's displayed correctly.

[TentativeConvert]

This should be part of the wider work package “Clean up css”. I don't think fonts are specified consistently, unless someone has recently worked on this. As for the choice of font, there's a long discussion on Zulip about fonts with sufficient unicode coverage, which seems to have temporarily settled on Henrik Böving's choice of the following fonts on the community doc pages:

code font: JuliaMono non-code font: Lato Medium

However, later in the same discussion, Henrik Böving does throw in Source Code Pro as an alternative:

Rustdoc uses: Source Code Pro for code Source Serif 4 for prose Fira Sans in a bunch of special locations like headlines etc.

So sticking with this font should also be fine as long as it's applied consistently and shipped with the website.

[TentativeConvert]

Another user has the same font issue on Safari on an iPad Pro.

[joneugster]

Hopefully, all code should now be JuliaMono and all non-code Roboto and both fonts are shipped with the page content if the user does not have them installed.