tuned;
authorFabian Huch <huch@in.tum.de>
Sat, 01 Feb 2025 22:41:43 +0100
changeset 82044 c16859834288
parent 82043 65ac068f9d17
child 82045 b8ba54ab790b
tuned;
src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Sat Feb 01 22:39:44 2025 +0100
+++ b/src/Pure/Build/build_manager.scala	Sat Feb 01 22:41:43 2025 +0100
@@ -1617,18 +1617,14 @@
 
   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(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")
 
     def task_dir(task: Task) = pending + Path.basic(task.uuid.toString)
-    def report(kind: String, id: Long): Report =
-      Report(kind, id, finished + Path.make(List(kind, id.toString)))
 
     def sync_permissions(dir: Path, ssh: SSH.System = SSH.Local): Unit = {
       ssh.execute("chmod -R g+rwx " + File.bash_path(dir))
@@ -1640,18 +1636,6 @@
 
     val ssh_group: String = options.string("build_manager_group")
 
-    def open_cluster_ssh(): SSH.Session =
-      SSH.open_session(options,
-        host = options.string("build_manager_cluster_ssh_host"),
-        port = options.int("build_manager_cluster_ssh_port"),
-        user = options.string("build_manager_cluster_ssh_user"))
-
-    def open_ssh(): SSH.Session =
-      SSH.open_session(options,
-        host = options.string("build_manager_ssh_host"),
-        port = options.int("build_manager_ssh_port"),
-        user = options.string("build_manager_ssh_user"))
-
     def open_database(server: SSH.Server = SSH.no_server): PostgreSQL.Database =
       PostgreSQL.open_database_server(options, server = server,
         user = options.string("build_manager_database_user"),
@@ -1663,6 +1647,30 @@
         ssh_port = options.int("build_manager_database_ssh_port"),
         ssh_user = options.string("build_manager_database_ssh_user"))
 
+
+    /* server */
+
+    val identifier = options.string("build_manager_identifier")
+
+    val finished = base_dir + Path.basic("finished")
+    def report(kind: String, id: Long): Report =
+      Report(kind, id, finished + Path.make(List(kind, id.toString)))
+
+    def open_cluster_ssh(): SSH.Session =
+      SSH.open_session(options,
+        host = options.string("build_manager_cluster_ssh_host"),
+        port = options.int("build_manager_cluster_ssh_port"),
+        user = options.string("build_manager_cluster_ssh_user"))
+
+
+    /* client */
+
+    def open_ssh(): SSH.Session =
+      SSH.open_session(options,
+        host = options.string("build_manager_ssh_host"),
+        port = options.int("build_manager_ssh_port"),
+        user = options.string("build_manager_ssh_user"))
+
     def open_postgresql_server(): SSH.Server =
       PostgreSQL.open_server(options,
         host = options.string("build_manager_database_host"),