[Factor-talk] how to join the Discord server (was: font sizes in browser und listener)

Hi, Le 21/09/2023 à 19:46, CW Alston a écrit : Hi -- Just joined Discord! How do I find the Factor server there? This link should work: https://discord.gg/QxJYZx3QDf -- Vivien (jmiven) ___ Factor-talk mailing list

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

https://discord.gg/QxJYZx3QDfOn Sep 21, 2023, at 10:48 AM, CW Alston wrote:Hi -- Just joined Discord! How do I find the Factor server there?On Thu, Sep 21, 2023 at 9:33 AM John Benediktsson wrote:Yes, and we would be happy to help assist.  A fair amount of developer

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

Hi -- Just joined Discord! How do I find the Factor server there? On Thu, Sep 21, 2023 at 9:33 AM John Benediktsson wrote: > Yes, and we would be happy to help assist. > > A fair amount of developer conversation takes place on the Discord server, > if you want more real-time chats about it. Or

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

Yes, and we would be happy to help assist. A fair amount of developer conversation takes place on the Discord server, if you want more real-time chats about it. Or on the Github issue I just opened: https://github.com/factor/factor/issues/2876 > On Sep 21, 2023, at 9:00 AM, Krisztián

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

*Is that something a newcomer can do?* Hello, This is my first post here. I've admired Factor for years, and reading its documentation once helped me grasp the concept of refactoring. However, I've never really used it. Do you think this issue would be a good starting point? Thanks, Krisztián

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

I suspect if you put those font lines in your .factor-boot-rc and bootstrap it will all look good. We must be caching the default font in places and need that to all be responsive to changes. On Thu, Sep 21, 2023 at 8:22 AM Georg Simon wrote: > Yes restart and yes new listener window. > > For

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

Yes restart and yes new listener window. For instance I can start the listener and enter "today". I get an error message with two tiny lines. I choose "Use the calendar vocabulary" and get some more tiny messages. Am Thu, 21 Sep 2023 08:04:48 -0700 schrieb John Benediktsson : > Did you restart

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

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 : > The quickest way is to change the default-font-size in the fonts > vocab to be larger. > > IN: fonts > CONSTANT: default-font-size 36 >