# HG changeset patch
# User wenzelm
# Date 1520013475 -3600
# Node ID cb0f0f5f88764c035332506d73aa5603e8be1553
# Parent  d83efbe524383291caa32aa458fbe38e4ce865d7
more ssh options;

diff -r d83efbe52438 -r cb0f0f5f8876 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Fri Mar 02 18:45:11 2018 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri Mar 02 18:57:55 2018 +0100
@@ -114,6 +114,10 @@
     host: String,
     user: String = "",
     port: Int = 0,
+    ssh_host: String = "",
+    proxy_host: String = "",
+    proxy_user: String = "",
+    proxy_port: Int = 0,
     shared_home: Boolean = true,
     historic: Boolean = false,
     history: Int = 0,
@@ -282,7 +286,9 @@
     val task_name = "build_history-" + r.host
     Logger_Task(task_name, logger =>
       {
-        using(logger.ssh_context.open_session(host = r.host, user = r.user, port = r.port))(
+        using(logger.ssh_context.open_session(
+            host = proper_string(r.ssh_host) getOrElse r.host, user = r.user, port = r.port,
+            proxy_host = r.proxy_host, proxy_user = r.proxy_user, proxy_port = r.proxy_port))(
           ssh =>
             {
               val self_update = !r.shared_home