Fonts

The default font is now changed from "Bitstream Vera Sans" to "DejaVu Sans". The current font supports additional international, math, and symbol characters, including emojis.