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 <georg.si...@auge.de> 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 <mrj...@gmail.com>: > >> 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 <georg.si...@auge.de> >>> 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 >>> Factor-talk@lists.sourceforge.net >>> https://lists.sourceforge.net/lists/listinfo/factor-talk >> >> >> _______________________________________________ >> Factor-talk mailing list >> Factor-talk@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/factor-talk > > > > _______________________________________________ > Factor-talk mailing list > Factor-talk@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/factor-talk _______________________________________________ Factor-talk mailing list Factor-talk@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/factor-talk
