# HG changeset patch # User wenzelm # Date 1501940882 -7200 # Node ID 30663525e0577bb51f0ddd531c863fa9c2b04679 # Parent 1072edd475dcaebf7710ca3ec5943698901e88b4 default according to Java API, instead of jEdit usage; diff -r 1072edd475dc -r 30663525e057 src/Pure/System/system_channel.scala --- a/src/Pure/System/system_channel.scala Sat Aug 05 12:18:25 2017 +0200 +++ b/src/Pure/System/system_channel.scala Sat Aug 05 15:48:02 2017 +0200 @@ -18,7 +18,7 @@ class System_Channel private { - private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1")) + private val server = new ServerSocket(0, 50, InetAddress.getByName("127.0.0.1")) val server_name: String = "127.0.0.1:" + server.getLocalPort override def toString: String = server_name