more robust connection via proxy_host;
authorwenzelm
Sun, 15 Mar 2020 11:38:36 +0100
changeset 71554 2a82462276db
parent 71553 cf2406e654cf
child 71555 7eadccd4392c
more robust connection via proxy_host;
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 " +