Am 18.09.2013 um 16:51 schrieb Makarius <[email protected]>: > 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
