The font size is controlled by the browser so what you need to do varies by broswer. You need to figure out how to change default font info for your browser. Many browsers support ctrl+plus or minus keys to change font size. I find tuning it manually that way works well for me.
On Mon, Jul 2, 2012 at 11:26 PM, Murray Eisenberg <[email protected]>wrote: > The default font size in J is much too small for my eyes. > > For the iOS version of J, the verb jf easily changes font size. > > For a non-iOS jhs7, what command may be used to change the font size in > the jijx browser window (and other browser windows opened for J, e.g., > an ijs window)? > > In what startup configuration file should that command go. > > -- > Murray Eisenberg [email protected] > 80 Fearing Street phone 413 549-1020 (H) > Amherst, MA 01002-1912 > ---------------------------------------------------------------------- > For information about J forums see http://www.jsoftware.com/forums.htm > ---------------------------------------------------------------------- For information about J forums see http://www.jsoftware.com/forums.htm
