src/Pure/General/ssh.scala
changeset 64258 cdb38bb9a3f0
parent 64257 9d51ac055cec
child 64304 96bc94c87a81
--- 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)