src/Pure/General/ssh.scala
changeset 67273 c573cfb2c407
parent 67067 02729ced9b1e
child 67745 d83efbe52438
--- 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")) {