clarified;
authorwenzelm
Sat, 16 Jan 2021 19:25:20 +0100
changeset 73135 76bdfde8a579
parent 73134 8a8ffe78eee7
child 73136 ca17e9ebfdf1
clarified;
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 =