more ssh options;
authorwenzelm
Fri, 02 Mar 2018 18:57:55 +0100
changeset 67746 cb0f0f5f8876
parent 67745 d83efbe52438
child 67747 7b84ecd54d70
more ssh options;
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