# HG changeset patch
# User wenzelm
# Date 1584613674 -3600
# Node ID 03133befa33b35bfe9aa845f5bfbce1bca3de486
# Parent  8ddd558d3044f6baba0f38bd9ed7fb11c570f500
support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);

diff -r 8ddd558d3044 -r 03133befa33b src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Wed Mar 18 22:22:16 2020 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Mar 19 11:27:54 2020 +0100
@@ -147,6 +147,7 @@
   sealed case class Remote_Build(
     description: String,
     host: String,
+    actual_host: String = "",
     user: String = "",
     port: Int = 0,
     proxy_host: String = "",
@@ -165,7 +166,7 @@
     active: Boolean = true)
   {
     def ssh_session(context: SSH.Context): SSH.Session =
-      context.open_session(host = host, user = user, port = port,
+      context.open_session(host = host, user = user, port = port, actual_host = actual_host,
         proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port,
         permissive = proxy_host.nonEmpty)
 
@@ -337,7 +338,7 @@
   val remote_builds2: List[List[Remote_Build]] =
     List(
       List(
-        Remote_Build("AFP2", "lrzcloud2", self_update = true,
+        Remote_Build("AFP2", "lrzcloud2", actual_host = "10.195.2.10", self_update = true,
           proxy_host = "lxbroy10", proxy_user = "i21isatest",
           options = "-m32 -M1x8 -t AFP" +
             " -e ISABELLE_GHC=ghc" +
@@ -347,7 +348,7 @@
           args = "-a -X large -X slow",
           afp = true,
           detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")),
-        Remote_Build("AFP bulky2", "lrzcloud2", self_update = true,
+        Remote_Build("AFP bulky2", "lrzcloud2", actual_host = "10.195.2.10", self_update = true,
           proxy_host = "lxbroy10", proxy_user = "i21isatest",
           options = "-m64 -M8 -U30000 -s10 -t AFP",
           args = "-g large -g slow",
diff -r 8ddd558d3044 -r 03133befa33b src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Wed Mar 18 22:22:16 2020 +0100
+++ b/src/Pure/General/ssh.scala	Thu Mar 19 11:27:54 2020 +0100
@@ -83,10 +83,12 @@
     new Context(options, jsch)
   }
 
-  def open_session(options: Options, host: String, user: String = "", port: Int = 0,
+  def open_session(options: Options,
+      host: String, user: String = "", port: Int = 0, actual_host: String = "",
       proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0,
       permissive: Boolean = false): Session =
-    init_context(options).open_session(host = host, user = user, port = port,
+    init_context(options).open_session(
+      host = host, user = user, port = port, actual_host = actual_host,
       proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port,
       permissive = permissive)
 
@@ -120,16 +122,18 @@
         proper_string(nominal_user) getOrElse user)
     }
 
-    def open_session(host: String, user: String = "", port: Int = 0,
+    def open_session(
+      host: String, user: String = "", port: Int = 0, actual_host: String = "",
       proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0,
       permissive: Boolean = false): Session =
     {
-      if (proxy_host == "") connect_session(host = host, user = user, port = port)
+      val connect_host = proper_string(actual_host) getOrElse host
+      if (proxy_host == "") connect_session(host = connect_host, user = user, port = port)
       else {
         val proxy = connect_session(host = proxy_host, port = proxy_port, user = proxy_user)
 
         val fw =
-          try { proxy.port_forwarding(remote_host = host, remote_port = make_port(port)) }
+          try { proxy.port_forwarding(remote_host = connect_host, remote_port = make_port(port)) }
           catch { case exn: Throwable => proxy.close; throw exn }
 
         try {