# HG changeset patch
# User wenzelm
# Date 1585658456 -7200
# Node ID ec14ef6dd09bcaf986852a659fe0f6af96bd7fc6
# Parent  45c2b8cf1b26f086b87da99b66e1501e6f523b96
close socket explicitly (idempotent);

diff -r 45c2b8cf1b26 -r ec14ef6dd09b src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Mar 31 14:09:36 2020 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Mar 31 14:40:56 2020 +0200
@@ -204,6 +204,8 @@
     val _ = Future.shutdown ();
     val _ = Execution.reset ();
     val _ = Message_Channel.shutdown msg_channel;
+    val _ = BinIO.closeIn in_stream;
+    val _ = BinIO.closeOut out_stream;
 
   in Exn.release result end);