Email Gateway (Aug 22 2022 at 12:39): Email Gateway (Aug 22 2022 at 12:39):From: Thomas Sternagel <Thomas.Sternagel@uibk.ac.at>
Just switched to RC5. First thing I noticed was that Ctrl+E Uparrow and
Ctrl+E Downarrow do not work for me anymore. I don't think that I
changed any settings between RC4 and RC5.
Cheers,
Tom
Email Gateway (Aug 22 2022 at 12:39):From: Makarius <makarius@sketis.net>
I did not change anything here.
Maybe it is just a confusion of $ISABELLE_HOME_USER/jedit configuration,
notably keymaps/imported_keys.props that are generated from Isabelle/jEdit
default properties only for a fresh situation.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC