# HG changeset patch
# User wenzelm
# Date 1700857952 -3600
# Node ID c83cdd300848fdccb56dae206e7ebfa33fa6616a
# Parent  edc0dbd59d484cef6e0bca234ef03373f297d7cf
clarified buffer_size;

diff -r edc0dbd59d48 -r c83cdd300848 src/Pure/System/system_channel.scala
--- a/src/Pure/System/system_channel.scala	Fri Nov 24 20:58:29 2023 +0100
+++ b/src/Pure/System/system_channel.scala	Fri Nov 24 21:32:32 2023 +0100
@@ -8,7 +8,8 @@
 
 
 import java.io.{InputStream, OutputStream}
-import java.net.{InetAddress, InetSocketAddress, ProtocolFamily, ServerSocket, SocketAddress, StandardProtocolFamily, UnixDomainSocketAddress}
+import java.net.{InetAddress, InetSocketAddress, ProtocolFamily, ServerSocket, SocketAddress,
+  StandardProtocolFamily, UnixDomainSocketAddress, StandardSocketOptions}
 import java.nio.channels.{ServerSocketChannel, Channels}
 
 
@@ -16,8 +17,11 @@
   def apply(unix_domain: Boolean = false): System_Channel =
     if (unix_domain) new Unix else new Inet
 
+  val buffer_size: Integer = Integer.valueOf(131072)
+
   class Inet extends System_Channel(StandardProtocolFamily.INET) {
     server.bind(new InetSocketAddress(Server.localhost, 0), 50)
+    server.setOption(StandardSocketOptions.SO_RCVBUF, buffer_size)
 
     override def address: String =
       Server.print_address(server.getLocalAddress.asInstanceOf[InetSocketAddress].getPort)
@@ -28,6 +32,7 @@
     private val socket_file_name = socket_file.getPath
 
     server.bind(UnixDomainSocketAddress.of(socket_file_name))
+    server.setOption(StandardSocketOptions.SO_RCVBUF, buffer_size)
 
     override def address: String = socket_file_name
     override def shutdown(): Unit = {