<p>Isn't the settings dialogue for font replacement is for? I am not in front of it now, but I remember there is a font substitution setting somewhere...</p>
<p>Amichai.<br>
</p>
<div class="gmail_quote">On Jan 22, 2012 5:35 PM, "Nadav Har&apos;El" <<a href="mailto:nyh@math.technion.ac.il">nyh@math.technion.ac.il</a>> wrote:<br type="attribution"></div>