# HG changeset patch
# User wenzelm
# Date 1495210255 -7200
# Node ID 326c9f828c3dcfc6cfe57a67a69da54c6e9dd65e
# Parent  12c90c0c4b323db80937a84c84d05a7cae5fd1a6
tuned;

diff -r 12c90c0c4b32 -r 326c9f828c3d src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Fri May 19 18:10:19 2017 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Fri May 19 18:10:55 2017 +0200
@@ -54,7 +54,8 @@
 
   private val console_stream = new OutputStream
   {
-    val buf = new StringBuilder
+    val buf = new StringBuilder(100)
+
     override def flush()
     {
       val s = buf.synchronized { val s = buf.toString; buf.clear; s }
@@ -65,8 +66,11 @@
       }
       Thread.sleep(10)  // FIXME adhoc delay to avoid loosing output
     }
+
     override def close() { flush () }
-    def write(byte: Int) {
+
+    def write(byte: Int)
+    {
       val c = byte.toChar
       buf.synchronized { buf.append(c) }
       if (c == '\n') flush()