# 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 =