src/Pure/General/ssh.scala

--- a/src/Pure/General/ssh.scala	Sat Apr 04 18:05:37 2020 +0200
+++ b/src/Pure/General/ssh.scala	Sat Apr 04 18:13:05 2020 +0200
@@ -237,7 +237,7 @@
 
     val exit_status: Future[Int] =
       Future.thread("ssh_wait") {
-        while (!channel.isClosed) Thread.sleep(exec_wait_delay.ms)
+        while (!channel.isClosed) exec_wait_delay.sleep
         channel.getExitStatus
       }
 
@@ -276,7 +276,7 @@
             if (line_buffer.size > 0) line_flush()
             finished = true
           }
-          else Thread.sleep(exec_wait_delay.ms)
+          else exec_wait_delay.sleep
         }
 
         result.toList