author | wenzelm |
Fri, 09 Aug 2013 20:30:11 +0200 | |
changeset 52948 | 383c1496d0aa |
parent 52947 | a7947b72bac2 |
child 52949 | 90edb0669845 |
--- a/src/Tools/jEdit/src/jEdit.props Fri Aug 09 20:26:54 2013 +0200 +++ b/src/Tools/jEdit/src/jEdit.props Fri Aug 09 20:30:11 2013 +0200 @@ -179,6 +179,7 @@ insert-newline-indent.shortcut= insert-newline.shortcut=ENTER isabelle-documentation.dock-position=right +isabelle-find.dock-position=bottom isabelle-output.dock-position=bottom isabelle-output.height=174 isabelle-output.width=412