# HG changeset patch
# User wenzelm
# Date 1584268716 -3600
# Node ID 2a82462276db37738d426da3f051a2fbef7225e7
# Parent  cf2406e654cf65e4a712c4fd5a650eb7f2894596
more robust connection via proxy_host;

diff -r cf2406e654cf -r 2a82462276db src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Mar 14 21:58:29 2020 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun Mar 15 11:38:36 2020 +0100
@@ -150,7 +150,6 @@
     user: String = "",
     port: Int = 0,
     ssh_host: String = "",
-    ssh_permissive: Boolean = false,
     proxy_host: String = "",
     proxy_user: String = "",
     proxy_port: Int = 0,
@@ -169,7 +168,7 @@
     def ssh_session(context: SSH.Context): SSH.Session =
       context.open_session(host = proper_string(ssh_host) getOrElse host, user = user, port = port,
         proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port,
-        permissive = ssh_permissive)
+        permissive = proxy_host.nonEmpty)
 
     def sql: SQL.Source =
       Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +