It shouldn't be necessary, since it was basically specifying a
font that may or may not be installed on folks' computers (and
wasn't loaded from the CSS). Tiny simplification but I'll take it 😁
This was discussed and agreed in #246. It will probably break a few
outstanding PRs as well as a few external links but it's for the
better good long term.