--- 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;
--- 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)
}