more generous timeout;
authorwenzelm
Fri, 09 Mar 2018 15:09:08 +0100
changeset 67798 d327558f776a
parent 67797 1cfc7541012e
child 67799 f801cb14a0b3
more generous timeout;
src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Fri Mar 09 15:06:35 2018 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 09 15:09:08 2018 +0100
@@ -110,7 +110,7 @@
         try {
           using(connection())(connection =>
             {
-              connection.socket.setSoTimeout(500)
+              connection.socket.setSoTimeout(2000)
               connection.read_line() == Some(Reply.OK.toString)
             })
         }