src/Pure/General/socket_io.ML

--- a/src/Pure/General/socket_io.ML	Thu Oct 04 15:25:58 2018 +0100
+++ b/src/Pure/General/socket_io.ML	Thu Oct 04 16:40:03 2018 +0200
@@ -79,7 +79,6 @@
       | _ => 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;