Re: [Factor-talk] font sizes in browser und listener

[John B. <mr...@gm...>]

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 <geo...@au...> 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 <mr...@gm...>:
> 
>> 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 <geo...@au...>
>>> 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
>>> Fac...@li...
>>> https://lists.sourceforge.net/lists/listinfo/factor-talk  
>> 
>> 
>> _______________________________________________
>> Factor-talk mailing list
>> Fac...@li...
>> https://lists.sourceforge.net/lists/listinfo/factor-talk
> 
> 
> 
> _______________________________________________
> Factor-talk mailing list
> Fac...@li...
> https://lists.sourceforge.net/lists/listinfo/factor-talk