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)