prevent sporadic disconnection;
authorwenzelm
Thu Oct 20 23:05:13 2016 +0200 (2016-10-20)
changeset 6432547e03cb99274
parent 64324 416f4d031afd
child 64326 ff3c383b9163
prevent sporadic disconnection;
etc/options
src/Pure/General/ssh.scala
     1.1 --- a/etc/options	Thu Oct 20 16:29:02 2016 +0200
     1.2 +++ b/etc/options	Thu Oct 20 23:05:13 2016 +0200
     1.3 @@ -206,3 +206,6 @@
     1.4  
     1.5  option ssh_connect_timeout : real = 60
     1.6    -- "SSH connection timeout (seconds)"
     1.7 +
     1.8 +option ssh_alive_interval : real = 30
     1.9 +  -- "time interval to keep SSH server connection alive (seconds)"
     2.1 --- a/src/Pure/General/ssh.scala	Thu Oct 20 16:29:02 2016 +0200
     2.2 +++ b/src/Pure/General/ssh.scala	Thu Oct 20 23:05:13 2016 +0200
     2.3 @@ -41,6 +41,9 @@
     2.4    def connect_timeout(options: Options): Int =
     2.5      options.seconds("ssh_connect_timeout").ms.toInt
     2.6  
     2.7 +  def alive_interval(options: Options): Int =
     2.8 +    options.seconds("ssh_alive_interval").ms.toInt
     2.9 +
    2.10  
    2.11    /* init context */
    2.12  
    2.13 @@ -76,6 +79,7 @@
    2.14        val session = jsch.getSession(if (user == "") null else user, host, port)
    2.15  
    2.16        session.setUserInfo(No_User_Info)
    2.17 +      session.setServerAliveInterval(alive_interval(options))
    2.18        session.setConfig("MaxAuthTries", "3")
    2.19  
    2.20        if (options.bool("ssh_compression")) {