--- 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