# HG changeset patch
# User wenzelm
# Date 1663016637 -7200
# Node ID 4a0b7151fedc47f0b19f724e286b73145fde389b
# Parent  b8f26c20d3b1cb563e5b3d9ced519eadc101cd10
removed remains of proxy_host management: delegated to .ssh/config;

diff -r b8f26c20d3b1 -r 4a0b7151fedc src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Mon Sep 12 22:52:15 2022 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Mon Sep 12 23:03:57 2022 +0200
@@ -135,7 +135,6 @@
   sealed case class Remote_Build(
     description: String,
     host: String,
-    actual_host: String = "",
     user: String = "",
     port: Int = 0,
     historic: Boolean = false,
@@ -151,7 +150,7 @@
     active: Boolean = true
   ) {
     def open_session(options: Options): SSH.Session =
-      SSH.open_session(options, host = host, user = user, port = port, actual_host = actual_host)
+      SSH.open_session(options, host = host, user = user, port = port)
 
     def sql: PostgreSQL.Source =
       Build_Log.Prop.build_engine.toString + " = " + SQL.string(Build_History.engine) + " AND " +
@@ -345,8 +344,7 @@
           options = "-m32 -M4 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs",
           detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"))),
       List(
-        Remote_Build("macOS 10.15 Catalina", "monterey", actual_host = "laramac01",
-          user = "makarius",
+        Remote_Build("macOS 10.15 Catalina", "monterey", user = "makarius",
           options = "-m32 -M4 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
           args = "-a -d '~~/src/Benchmarks'")),
       List(
@@ -373,7 +371,7 @@
   val remote_builds2: List[List[Remote_Build]] =
     List(
       List(
-        Remote_Build("AFP", "lrzcloud2", actual_host = "10.195.4.41",
+        Remote_Build("AFP", "lrzcloud2",
           java_heap = "8g",
           options = "-m32 -M1x6 -t AFP" +
             " -e ISABELLE_GHC=ghc" +
@@ -383,7 +381,7 @@
           args = "-a -X large -X slow",
           afp = true,
           detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")),
-        Remote_Build("AFP", "lrzcloud2", actual_host = "10.195.4.41",
+        Remote_Build("AFP", "lrzcloud2",
           java_heap = "8g",
           options = "-m64 -M8 -U30000 -s10 -t AFP",
           args = "-g large -g slow",
diff -r b8f26c20d3b1 -r 4a0b7151fedc src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon Sep 12 22:52:15 2022 +0200
+++ b/src/Pure/General/ssh.scala	Mon Sep 12 23:03:57 2022 +0200
@@ -94,12 +94,8 @@
     host: String,
     port: Int = 0,
     user: String = "",
-    actual_host: String = "",
     multiplex: Boolean = !Platform.is_windows
   ): Session = {
-    val session_host = proper_string(actual_host) getOrElse host
-    val session_port = make_port(port)
-
     val (control_master, control_path) =
       if (multiplex) {
         val file = Isabelle_System.tmp_file("ssh_socket")
@@ -108,7 +104,7 @@
       }
       else (false, "")
 
-    new Session(options, session_host, session_port, user, control_master, control_path)
+    new Session(options, host, make_port(port), user, control_master, control_path)
   }
 
   class Session private[SSH](