use ssh host for default address;
authorFabian Huch <huch@in.tum.de>
Sat, 01 Feb 2025 22:39:44 +0100
changeset 82043 65ac068f9d17
parent 82042 d064d6f36ce1
child 82044 c16859834288
use ssh host for default address;
etc/options
src/Pure/Build/build_manager.scala
--- 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"
--- 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")