changeset 54340 | 18c621069bf8 |
parent 54339 | 26c790a6ce43 |
child 54342 | fbcaa9f08879 |
--- 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;