# HG changeset patch
# User wenzelm
# Date 1381916922 -7200
# Node ID 18c621069bf86c084fecd0bed5713f948461746a
# Parent  26c790a6ce435f4b6d17ed4f0d2bfd4ec45ddc58
prefer TCP_NODELAY -- avoid extra buffering due to Nagle's algorithm;

diff -r 26c790a6ce43 -r 18c621069bf8 src/Pure/General/socket_io.ML
--- a/src/Pure/General/socket_io.ML	Wed Oct 16 11:35:04 2013 +0200
+++ b/src/Pure/General/socket_io.ML	Wed Oct 16 11:48:42 2013 +0200
@@ -81,6 +81,7 @@
       | _ => err ());
     val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
     val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
+    val _ = INetSock.TCP.setNODELAY (socket, true);
   in make_streams socket end;
 
 end;
diff -r 26c790a6ce43 -r 18c621069bf8 src/Pure/System/system_channel.scala
--- a/src/Pure/System/system_channel.scala	Wed Oct 16 11:35:04 2013 +0200
+++ b/src/Pure/System/system_channel.scala	Wed Oct 16 11:48:42 2013 +0200
@@ -86,6 +86,7 @@
   def rendezvous(): (OutputStream, InputStream) =
   {
     val socket = server.accept
+    socket.setTcpNoDelay(true)
     (socket.getOutputStream, socket.getInputStream)
   }