21 Aug
2014
21 Aug
'14
2:34 a.m.
Tudor Girba wrote:
That is great to hear.
@Sean: Just print out the result of:
StandardFonts defaultFont
Or look in the Settings/Appearange/Standard Fonts
If you see DejaVu in there, you are likely using a Bitmap font.
Doru
Ahhh. I had seen DejaVu and assumed it was Truetype. How is a TrueType
DejaVu font distinguished? Could it be possible to name strikefonts
DejaVu-StrikeFont?
cheers -ben