Of course I know how to change font size for any window in my browser (Safari under OS X). But since the J browser window is just displaying html, surely there is -- or could be -- some way for J itself to change what's the default font size there.
Isn't that what a And isn't this essentially what's being done when one uses "jf" for the iOS version of J? The fact is, for nearly every web site I visit with Safari, including jwiki and other pages at jsoftware.com, the default font size is just fine, even on my 27" hi-res iMac. But for the jhs browser window the font is by default just too, too small and thin to be comfortably readable. On 7/3/12 10:03 AM, Eric Iverson <[email protected]> wrote: > > 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] Mathematics & Statistics Dept. Lederle Graduate Research Tower phone 413 549-1020 (H) University of Massachusetts 413 545-2859 (W) 710 North Pleasant Street fax 413 545-1801 Amherst, MA 01003-9305 ---------------------------------------------------------------------- For information about J forums see http://www.jsoftware.com/forums.htm
