<https://sourceforge.net/p/testlilyissues/issues/4771/> made me think
that we really should specify a default font for our web site. Else the
browser will be left to choose, eventually presenting the user with
Times New Roman, if he hasn’t made a better choice yet. Shouldn’t we
avoid that?
If yes, the question is: which font should we use? Personally, I adore
Garamond, which is also sufficiently ‘classical’. But I imagine it would
also make sense to use the same default as we use when engraving music,
i.e. TeX Gyre Schola.