# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# 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")