# HG changeset patch
# User wenzelm
# Date 1520848852 -3600
# Node ID 3ded4e0bc54b4bee02169eda9065d559742c3e90
# Parent  e135d03f656f1837ccb18827a983ce28cfcfddf2
tuned;

diff -r e135d03f656f -r 3ded4e0bc54b src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Mon Mar 12 10:55:02 2018 +0100
+++ b/src/Pure/Tools/server.scala	Mon Mar 12 11:00:52 2018 +0100
@@ -184,11 +184,6 @@
         case _: SocketException => false
         case _: SocketTimeoutException => false
       }
-
-    def console(interrupt: Option[() => Unit] = None)
-    {
-      using(connection())(connection => connection.tty_loop(interrupt = interrupt).join)
-    }
   }
 
 
@@ -324,7 +319,9 @@
       else {
         val (server_info, server) = init(name, port = port, existing_server = existing_server)
         Output.writeln(server_info.toString, stdout = true)
-        if (console) server_info.console()
+        if (console) {
+          using(server_info.connection())(connection => connection.tty_loop().join)
+        }
         server.foreach(_.join)
       }
     })