We ship our own font to not have to depend on the host system's
installed fonts for 'special' characters like arrows and stars.
This is a font forked from the Gnu-free font people, only since that one
is 2MB this is a very much stripped down version with just all the fun
stuff left.
