[isabelle-dev] Missing letters in jEdit

Jasmin Blanchette jasmin.blanchette at gmail.com
Wed Sep 18 17:27:12 CEST 2013

Previous message (by thread): [isabelle-dev] Missing letters in jEdit
Next message (by thread): [isabelle-dev] Missing letters in jEdit
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

Am 18.09.2013 um 16:51 schrieb Makarius <makarius at sketis.net>:

> OK, just a few more details: The jEdit Global Options / Text Area pane has various "tuning parameters" that affect the font style.  What are your preferences for the following?
> 
>  Anti Aliased smooth text
>  Fractional font metrics

"standard" and unchecked, respectively.

Jasmin

Previous message (by thread): [isabelle-dev] Missing letters in jEdit
Next message (by thread): [isabelle-dev] Missing letters in jEdit
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

More information about the isabelle-dev mailing list