Re: [Factor-talk] Adjust font sizes in Listener and Help Browser

2017-06-06 Thread John Benediktsson
It's not elegant (because it's only for Listener and Browser, and different for each one), but there is a way to do that for the Listener and Browser. In the Listener, for example: IN: scratchpad "monospace" 20 set-listener-font In the Browser: Ctrl "plus" to increase font size (Ctrl

[Factor-talk] Adjust font sizes in Listener and Help Browser

2017-06-06 Thread Sankaranarayanan Viswanathan
Hi Guys, Is there a way to increase the font-size of the UI globally? Thanks, Sankar -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot