# HG changeset patch # User wenzelm # Date 1472633370 -7200 # Node ID fb0ae6b604910ce32d6fd917a35f8a09940c50bd # Parent 133e3e84e6fb962e66196c1db20d9b94df0de702 clarified (see 019856db2bb6, ea52509f4c42); diff -r 133e3e84e6fb -r fb0ae6b60491 src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Tue Aug 30 21:56:14 2016 +0200 +++ b/src/Tools/jEdit/src/jEdit.props Wed Aug 31 10:49:30 2016 +0200 @@ -184,7 +184,7 @@ gatchan.highlight.overview=false home.shortcut= insert-newline-indent.shortcut= -insert-newline.shortcut=ENTER +insert-newline.shortcut= isabelle-debugger.dock-position=floating isabelle-documentation.dock-position=right isabelle-output.dock-position=bottom