# HG changeset patch
# User wenzelm
# Date 1476633145 -7200
# Node ID cdb38bb9a3f020c234e01d70368d69faf95f791e
# Parent  9d51ac055cecb8255488bc7bce0dba49dcff98cf
removed useless operation -- would require bash_process wrapper;

diff -r 9d51ac055cec -r cdb38bb9a3f0 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)