author | wenzelm |
Thu, 03 Jun 2010 22:54:33 +0200 | |
changeset 37308 | 6e44af45b8c5 |
parent 37307 | 6dce93f3157d |
child 37309 | 38ce84c83738 |
src/Tools/jEdit/dist-template/properties/jedit.props | file | annotate | diff | comparison | revisions |
--- a/src/Tools/jEdit/dist-template/properties/jedit.props Thu Jun 03 22:45:49 2010 +0200 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props Thu Jun 03 22:54:33 2010 +0200 @@ -181,7 +181,7 @@ insert-newline-indent.shortcut= insert-newline.shortcut=ENTER isabelle-output.dock-position=bottom -isabelle-protocol.dock-position=bottom +isabelle-raw-output.dock-position=bottom isabelle.activate.shortcut=CS+ENTER line-end.shortcut=END line-home.shortcut=HOME