[chuck-users] mini shortcuts mistery

Fellow ChucKists, dear Spencer. For me the mini on Linux, using the Gnome desktop, has lately been acting up. Shortcuts like ctrl-c, ctrl-v, ctrl-x stop working after a while, so do the ones for adding and replacing shreds. Strangely ctrl-d *does* work in this state. No other programs have shown this behaviour and it's not consistent; they disappear after a while and so far I haven't seen them return. I think only the latest version does this. I'd like to document under what conditions this happens but it's quite inconsistent. Yours, Kas.