default according to Java API, instead of jEdit usage;
authorwenzelm
Sat, 05 Aug 2017 15:48:02 +0200
changeset 66346 30663525e057
parent 66341 1072edd475dc
child 66347 23eaab37e4a8
default according to Java API, instead of jEdit usage;
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