# HG changeset patch
# User wenzelm
# Date 1476997513 -7200
# Node ID 47e03cb9927458fdd72f2405bfe2d45f7c570f46
# Parent  416f4d031afd59a5edee50570d237cf1488c6f15
prevent sporadic disconnection;

diff -r 416f4d031afd -r 47e03cb99274 etc/options
--- 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)"
diff -r 416f4d031afd -r 47e03cb99274 src/Pure/General/ssh.scala
--- 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")) {