Re: [isabelle] Isabelle2019-RC0: isabelle_fonts_hinted has no effect



On 08/04/2019 23:18, Bertram Felgenhauer via Cl-isabelle-users wrote:
> 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.

OK, I will improve on that.

Note that it does not refer to Isabelle2019-RC0, but to a repository
version after it. There will be no further RC previews on isabelle-users
before official RC1 at the start of May-2019.


	Makarius





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