removed useless operation -- would require bash_process wrapper;
authorwenzelm
Sun, 16 Oct 2016 17:52:25 +0200
changeset 64258 cdb38bb9a3f0
parent 64257 9d51ac055cec
child 64259 eb476ea7bbea
removed useless operation -- would require bash_process wrapper;
src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sun Oct 16 17:50:40 2016 +0200
+++ b/src/Pure/General/ssh.scala	Sun Oct 16 17:52:25 2016 +0200
@@ -146,8 +146,6 @@
 
     def close() { channel.disconnect }
 
-    def kill(signal: String) { channel.sendSignal(signal) }
-
     val exit_status: Future[Int] =
       Future.thread("ssh_wait") {
         while (!channel.isClosed) Thread.sleep(exec_wait_delay.ms)