# HG changeset patch # User Fabian Huch # Date 1754491918 -7200 # Node ID b7422567c50753366acfea73330c35d56e78a8fe # Parent cbf3703f92ea409c2ff138c08ce18fb51397b0aa tuned doc: display build manager SSH options; diff -r cbf3703f92ea -r b7422567c507 etc/options --- a/etc/options Wed Aug 06 10:01:05 2025 +0100 +++ b/etc/options Wed Aug 06 16:51:58 2025 +0200 @@ -494,9 +494,11 @@ section "Build Manager SSH" option build_manager_ssh_host : string = "build.proof.cit.tum.de" for connection + -- "SSH host name for build manager" option build_manager_ssh_port : int = 0 for connection + -- "explicit SSH port" option build_manager_ssh_user : string = "" for connection - -- "ssh user to access build manager system" + -- "explicit SSH user" option build_manager_cluster_ssh_host : string = "localhost" for connection option build_manager_cluster_ssh_user : string = "" for connection diff -r cbf3703f92ea -r b7422567c507 src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Wed Aug 06 10:01:05 2025 +0100 +++ b/src/Pure/Build/build_manager.scala Wed Aug 06 16:51:58 2025 +0200 @@ -1942,6 +1942,9 @@ /* Isabelle tool wrapper */ + private val build_manager_ssh_options = + List("build_manager_ssh_user", "build_manager_ssh_host", "build_manager_ssh_port") + val isabelle_tool2 = Isabelle_Tool("build_task", "submit build task for build manager", Scala_Project.here, { args => @@ -1962,6 +1965,9 @@ var rev = "" val exclude_sessions = new mutable.ListBuffer[String] + def show_options: String = + cat_lines(build_manager_ssh_options.flatMap(options.get).map(_.print)) + val getopts = Getopts(""" Usage: isabelle build_task [OPTIONS] [SESSIONS ...] @@ -1978,14 +1984,16 @@ -f fresh build -g NAME select session group NAME -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) - -p OPTION override Isabelle system OPTION for build process (via NAME=VAL or NAME) + -p OPTION override Isabelle system OPTION for build process + (via NAME=VAL or NAME) -r REV explicit revision (default: state of working directory) -v verbose -x NAME exclude session NAME and all descendants - Submit build task on SSH server. Notable system options: + Submit build task on managed server. -""" + Library.indent_lines(2, options.get("build_manager_ssh_user").get.print) + "\n", + Requires SSH access to known host according to system options: +""" + Library.indent_lines(4, show_options) + "\n", "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))), "B:" -> (arg => base_sessions += arg), "P" -> (_ => presentation = true),