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