src/Pure/General/ssh.scala
changeset 64325 47e03cb99274
parent 64306 7b6dc1b36f20
child 64326 ff3c383b9163
--- a/src/Pure/General/ssh.scala	Thu Oct 20 16:29:02 2016 +0200
+++ b/src/Pure/General/ssh.scala	Thu Oct 20 23:05:13 2016 +0200
@@ -41,6 +41,9 @@
   def connect_timeout(options: Options): Int =
     options.seconds("ssh_connect_timeout").ms.toInt
 
+  def alive_interval(options: Options): Int =
+    options.seconds("ssh_alive_interval").ms.toInt
+
 
   /* init context */
 
@@ -76,6 +79,7 @@
       val session = jsch.getSession(if (user == "") null else user, host, port)
 
       session.setUserInfo(No_User_Info)
+      session.setServerAliveInterval(alive_interval(options))
       session.setConfig("MaxAuthTries", "3")
 
       if (options.bool("ssh_compression")) {