Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2019-RC0: isabelle_fonts_hinted has no...

Email Gateway (Aug 22 2022 at 19:37):

From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
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

Email Gateway (Aug 22 2022 at 19:38):

From: Makarius <makarius@sketis.net>
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

Last updated: Apr 18 2024 at 04:17 UTC