Did you restart Factor after saving? Or open a new listener window? I noticed the tips of the day at the top don’t properly grow in size and that needs to be fixed.
> On Sep 21, 2023, at 7:19 AM, Georg Simon <[email protected]> wrote: > > Thank you, much better now. > Only the messages printed by the listener are still tiny. > > Am Tue, 19 Sep 2023 06:27:45 -0700 > schrieb John Benediktsson <[email protected]>: > >> The quickest way is to change the default-font-size in the fonts >> vocab to be larger. >> >> IN: fonts >> CONSTANT: default-font-size 36 >> “help.stylesheet” reload >> save >> >> >>> On Sep 19, 2023, at 12:56 AM, Georg Simon <[email protected]> >>> wrote: >>> >>> Using now 2560x1600 pixels I would like to change all font sizes >>> permanently, menu bar and search field included. >>> >>> Thanks, Georg >>> >>> >>> _______________________________________________ >>> Factor-talk mailing list >>> [email protected] >>> https://lists.sourceforge.net/lists/listinfo/factor-talk >> >> >> _______________________________________________ >> Factor-talk mailing list >> [email protected] >> https://lists.sourceforge.net/lists/listinfo/factor-talk > > > > _______________________________________________ > Factor-talk mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/factor-talk _______________________________________________ Factor-talk mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/factor-talk
