# HG changeset patch # User Fabian Huch # Date 1738445984 -3600 # Node ID 65ac068f9d178c005fff1e1995f7369f950a0ba2 # Parent d064d6f36ce1a7386445c7a33739143dd72d0001 use ssh host for default address; diff -r d064d6f36ce1 -r 65ac068f9d17 etc/options --- a/etc/options Sat Feb 01 22:31:19 2025 +0100 +++ b/etc/options Sat Feb 01 22:39:44 2025 +0100 @@ -246,8 +246,8 @@ option build_manager_dir : string = "/srv/build" -- "directory for submissions on build server" -option build_manager_address : string = "https://build.proof.cit.tum.de" - -- "web address for build server" +option build_manager_address : string = "" + -- "explicit web address for build server" option build_manager_identifier : string = "build_manager" -- "isabelle identifier for build manager processes" diff -r d064d6f36ce1 -r 65ac068f9d17 src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Sat Feb 01 22:31:19 2025 +0100 +++ b/src/Pure/Build/build_manager.scala Sat Feb 01 22:39:44 2025 +0100 @@ -1618,7 +1618,10 @@ case class Store(options: Options) { val base_dir = Path.explode(options.string("build_manager_dir")) val identifier = options.string("build_manager_identifier") - val address = Url(options.string("build_manager_address")) + val address = { + Url(proper_string(options.string("build_manager_address")) getOrElse + "https://" + options.string("build_manager_ssh_host")) + } val pending = base_dir + Path.basic("pending") val finished = base_dir + Path.basic("finished")