src/Pure/Build/build_manager.scala
changeset 82043 65ac068f9d17
parent 82041 e7acf8c4572e
child 82044 c16859834288
--- 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")