# HG changeset patch # User wenzelm # Date 1610821520 -3600 # Node ID 76bdfde8a579a8512e03b5cf4631c5550d6a3054 # Parent 8a8ffe78eee7cf96ac349bffe99bbdcd8a018244 clarified; diff -r 8a8ffe78eee7 -r 76bdfde8a579 src/Pure/Tools/server.scala --- a/src/Pure/Tools/server.scala Sat Jan 16 17:02:14 2021 +0100 +++ b/src/Pure/Tools/server.scala Sat Jan 16 19:25:20 2021 +0100 @@ -189,7 +189,7 @@ catch { case _: IOException => None } def await_close(): Unit = - try { Byte_Message.read(in, 1) } + try { Byte_Message.read(in, 1); socket.close() } catch { case _: IOException => } def write_message(msg: String): Unit =