# HG changeset patch
# User wenzelm
# Date 1476130800 -7200
# Node ID 7c51914894579b56083281cf3d18b1fde56fa7fa
# Parent  865dda40e1cc534d97f39b346a04d5e0700a402b
close more thoroughly;

diff -r 865dda40e1cc -r 7c5191489457 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon Oct 10 21:52:55 2016 +0200
+++ b/src/Pure/General/ssh.scala	Mon Oct 10 22:20:00 2016 +0200
@@ -154,7 +154,7 @@
 
       def terminate()
       {
-        channel.disconnect
+        close
         out_lines.join
         err_lines.join
         exit_status.join
@@ -164,6 +164,7 @@
         try { exit_status.join }
         catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
 
+      close
       if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
 
       Process_Result(rc, out_lines.join, err_lines.join)