[chuck-users] Mini font resize bug (minor issue)

Dear fellow ChucKists (particularly Spencer), Some time ago I set the font of the Mini (latest version, ALSA, Linux, in this case) to have a huge size so I could easily demo something to a friend of mine. Now, I had to set it back and while the font got smaller immediately the cursor was still at the old (huge) height and so was the space between the lines. Re-starting the Mini fixed this issue. I'm not sure what the current best place to archive such bugs in the Mini is so sending it here. Yours, Kas.