# HG changeset patch
# User wenzelm
# Date 1538664003 -7200
#      Thu Oct 04 16:40:03 2018 +0200
# Node ID 9380c63aa8cf0cafc60620bea9758fdb2c0d0fed
# Parent  91162dd89571fb9ddfa36844fdb1a16aea13adcf
avoid TCP_NODELAY (in contrast to 18c621069bf8): might cause problems with some versions of Ubuntu 18.04;

diff -r 91162dd89571 -r 9380c63aa8cf src/Pure/General/socket_io.ML
--- a/src/Pure/General/socket_io.ML	Sun Aug 12 14:28:28 2018 +0200
+++ 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;
diff -r 91162dd89571 -r 9380c63aa8cf src/Pure/System/system_channel.scala
--- a/src/Pure/System/system_channel.scala	Sun Aug 12 14:28:28 2018 +0200
+++ b/src/Pure/System/system_channel.scala	Thu Oct 04 16:40:03 2018 +0200
@@ -26,7 +26,6 @@
   def rendezvous(): (OutputStream, InputStream) =
   {
     val socket = server.accept
-    socket.setTcpNoDelay(true)
     (socket.getOutputStream, socket.getInputStream)
   }