[isabelle] Isabelle2019-RC0: isabelle_fonts_hinted has no effect



Changing the 'Isabelle Fonts Hinted' option in the Isabelle plugin
settings has no effect; only the unhinted fonts are used.

The reason seems to be that the option is set by default, so it's
only stored if unset. But the isabelle_fonts component for a stored
'true' value instead.

Cheers,

Bertram





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.