# HG changeset patch
# User wenzelm
# Date 1548949444 -3600
# Node ID a8ee66876a1adac3e21eab9bd9f096f4ce849ad4
# Parent  efb0e5332441f76b681d62bacb4b6d10a8f23a46
tuned default layout;

diff -r efb0e5332441 -r a8ee66876a1a src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala	Thu Jan 31 16:33:57 2019 +0100
+++ b/src/Pure/Tools/main.scala	Thu Jan 31 16:44:04 2019 +0100
@@ -59,7 +59,7 @@
 <!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
 <PERSPECTIVE>
 <VIEW PLAIN="FALSE">
-<GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
+<GEOMETRY X="0" Y="35" WIDTH="1200" HEIGHT="850" EXT_STATE="0" />
 </VIEW>
 </PERSPECTIVE>""")
         }