# HG changeset patch # User wenzelm # Date 1547395045 -3600 # Node ID f044766cd94f47ea5829a6d26d4496629e4e0d5f # Parent 83f15deb2d36d09b508367a7a7d0f40cc77e2a58 File Browser is open by default; diff -r 83f15deb2d36 -r f044766cd94f src/Pure/Tools/main.scala --- a/src/Pure/Tools/main.scala Sun Jan 13 13:33:23 2019 +0100 +++ b/src/Pure/Tools/main.scala Sun Jan 13 16:57:25 2019 +0100 @@ -53,7 +53,7 @@ if (!(settings_dir + Path.explode("perspective.xml")).is_file) { File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"), - """""") + """""") File.write(settings_dir + Path.explode("perspective.xml"), """ diff -r 83f15deb2d36 -r f044766cd94f src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Sun Jan 13 13:33:23 2019 +0100 +++ b/src/Tools/jEdit/src/jEdit.props Sun Jan 13 16:57:25 2019 +0100 @@ -289,7 +289,7 @@ toggle-multi-select.shortcut2=C+NUMBER_SIGN toggle-rect-select.shortcut2=A+NUMBER_SIGN twoStageSave=false -vfs.browser.dock-position=floating +vfs.browser.dock-position=left vfs.favorite.0.type=1 vfs.favorite.0=$ISABELLE_HOME vfs.favorite.1.type=1