--- a/etc/options Thu Oct 20 16:29:02 2016 +0200
+++ b/etc/options Thu Oct 20 23:05:13 2016 +0200
@@ -206,3 +206,6 @@
option ssh_connect_timeout : real = 60
-- "SSH connection timeout (seconds)"
+
+option ssh_alive_interval : real = 30
+ -- "time interval to keep SSH server connection alive (seconds)"
--- 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")) {