tuned default perspective;
authorwenzelm
Thu, 03 Jun 2010 22:54:33 +0200
changeset 37308 6e44af45b8c5
parent 37307 6dce93f3157d
child 37309 38ce84c83738
tuned default perspective;
src/Tools/jEdit/dist-template/properties/jedit.props
--- 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