# HG changeset patch
# User wenzelm
# Date 1514116123 -3600
# Node ID c573cfb2c407d44a9b92bf7d1ec7a9dfc82a2708
# Parent  c41a032d8386e01e2f5608d963757ecee4de8896
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);

diff -r c41a032d8386 -r c573cfb2c407 etc/options
--- a/etc/options	Sat Dec 23 23:07:26 2017 +0100
+++ b/etc/options	Sun Dec 24 12:48:43 2017 +0100
@@ -238,6 +238,9 @@
 option ssh_alive_interval : real = 30
   -- "time interval to keep SSH server connection alive (seconds)"
 
+option ssh_alive_count_max : int = 3
+  -- "maximum number of messages to keep SSH server connection alive"
+
 
 section "Build Log Database"
 
diff -r c41a032d8386 -r c573cfb2c407 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sat Dec 23 23:07:26 2017 +0100
+++ b/src/Pure/General/ssh.scala	Sun Dec 24 12:48:43 2017 +0100
@@ -44,6 +44,9 @@
   def alive_interval(options: Options): Int =
     options.seconds("ssh_alive_interval").ms.toInt
 
+  def alive_count_max(options: Options): Int =
+    options.int("ssh_alive_count_max")
+
 
   /* init context */
 
@@ -85,6 +88,7 @@
 
       session.setUserInfo(No_User_Info)
       session.setServerAliveInterval(alive_interval(options))
+      session.setServerAliveCountMax(alive_count_max(options))
       session.setConfig("MaxAuthTries", "3")
 
       if (options.bool("ssh_compression")) {