# HG changeset patch
# User wenzelm
# Date 1520604548 -3600
# Node ID d327558f776a7f833c24c9ee4767f7d2051daa8f
# Parent  1cfc7541012e1a1c485c2090ac7e3e32bf0b1269
more generous timeout;

diff -r 1cfc7541012e -r d327558f776a 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)
             })
         }