--- 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",
--- 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](