> On 26 Aug 2016, at 3:29 AM, Richmond <richmondmathewson at gmail.com> wrote: > > Personally I find the teeny-weeny font size in the messageBox a bother: and I have had the font in the > scriptEditor set to 18 for the last 10 years. I’ll add that too as they should use the same font + size.