# HG changeset patch
# User wenzelm
# Date 1357766671 -3600
# Node ID 2d68df7ed89d10797c13bf410e911fb0689ee42f
# Parent  69810ebe120fbe32baf1e8774ca87a7418cc6980
Console is not docked on startup;

diff -r 69810ebe120f -r 2d68df7ed89d src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Wed Jan 09 21:59:53 2013 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Wed Jan 09 22:24:31 2013 +0100
@@ -7,6 +7,7 @@
 buffer.noTabs=true
 buffer.sidekick.keystroke-parse=false
 buffer.tabSize=2
+console.dock-position=floating
 console.encoding=UTF-8
 console.font=IsabelleText
 console.fontsize=14