tuned default layout;
authorwenzelm
Thu, 31 Jan 2019 16:44:04 +0100
changeset 69771 a8ee66876a1a
parent 69770 efb0e5332441
child 69772 ae1ef77746b5
tuned default layout;
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>""")
         }