Sat, 01 Dec 2012 22:42:54 +0100 | wenzelm | moved isabelle shortcuts to main jEdit.props, in order to have them migrated to the "imported" keymap; | changeset | files |
Sat, 01 Dec 2012 22:23:42 +0100 | wenzelm | leave ALTERNATIVE_DISPATCHER mostly enabled on Mac OS X, to get events for COMMAND/Meta combinations, which seem to produce only KEY_PRESSED in Java 7, not KEY_TYPED as in Java 6; | changeset | files |