On Thu, 29 Aug 2013, Ondřej Kunčar wrote:
This refers to 3c26a7042d8e. The numpad stopped working in JEdit.
Reproducible on my machine and also on Dmitriy's machine. We use Linux.
What exactly means stopped working? Can you give another changeset where
it still works, whatever that means here?
Note that I have recently changed many Isabelle/jEdit keyboard shortcuts.
This might cause some confusion with the persistent
$ISABELLE_HOME_USER/jedit/keymaps/ -- deleting that directory makes a
fresh start (and looses personal keybindings, if you have any).
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
