[isabelle] [SOLVED] jedit mouse offset/menu bug with fullscreen window managers

After a recent gnome upgrade, jedit suddenly stopped working for me: all
mouse clicks seemed to be offset by some amount, making menus unusable.
 A little googling established that this is a bug in the JVM, which
apparently contains a hardcoded list of window managers that don't add
window decorations, so that the swing/AWT can `work around' them (I've
got no idea why it feels it needs to, but it does).  The trigger (for
me) was that the name of the gnome window manager changed (from Mutter
to Gnome Shell), and thus no longer triggered the hack.  The solution
was to install the `wmname' utility, which lets you change the name that
the WM reports to clients - I set it back to Mutter, and everything
worked again.

I'm sending this around, as I'm guessing that others will probably run
across this behaviour at some point, and the solution might also make
jedit usable on other tiling WMs (xmonad, ratpoison, etc.).  The
long-term solution, of course, is a non-hacky JVM, but I'm not holding
my breath.



The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.