Re: [Factor-talk] font size in help browser

2020-11-27 Thread John Benediktsson
The easiest way, I suppose, to change all the font sizes is to increase this constant, and then refresh help.stylesheet, and restart: https://docs.factorcode.org/content/word-default-font-size,fonts.html We have a patch to make this a bit easier, but currently several of our libraries like the

[Factor-talk] font size in help browser

2020-11-27 Thread support
Hi everyone. I was wondering how would I change the font size in the help browser and generally the IDE under Windows. I don't really want to have to change the font size in all the other unrelated windows. TIA, -Kevin ___ Factor-talk mailing list Fact