tuned;
authorwenzelm
Mon, 12 Mar 2018 11:00:52 +0100
changeset 67834 3ded4e0bc54b
parent 67833 e135d03f656f
child 67835 c8e4ee2b5482
tuned;
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)
       }
     })