src/Pure/General/ssh.scala
changeset 73367 77ef8bef0593
parent 73340 0ffcad1f6130
child 73634 c88faa1e09e1
--- a/src/Pure/General/ssh.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/General/ssh.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -141,15 +141,15 @@
 
         val fw =
           try { proxy.port_forwarding(remote_host = connect_host, remote_port = make_port(port)) }
-          catch { case exn: Throwable => proxy.close; throw exn }
+          catch { case exn: Throwable => proxy.close(); throw exn }
 
         try {
           connect_session(host = fw.local_host, port = fw.local_port,
             host_key_permissive = permissive,
             nominal_host = host, nominal_user = user, user = user,
-            on_close = () => { fw.close; proxy.close })
+            on_close = () => { fw.close(); proxy.close() })
         }
-        catch { case exn: Throwable => fw.close; proxy.close; throw exn }
+        catch { case exn: Throwable => fw.close(); proxy.close(); throw exn }
       }
     }
   }
@@ -259,7 +259,7 @@
       progress_stderr: String => Unit = (_: String) => (),
       strict: Boolean = true): Process_Result =
     {
-      stdin.close
+      stdin.close()
 
       def read_lines(stream: InputStream, progress: String => Unit): List[String] =
       {
@@ -293,7 +293,7 @@
 
       def terminate(): Unit =
       {
-        close
+        close()
         out_lines.join
         err_lines.join
         exit_status.join
@@ -303,7 +303,7 @@
         try { exit_status.join }
         catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
 
-      close
+      close()
       if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
 
       Process_Result(rc, out_lines.join, err_lines.join)