diff -r 65ac068f9d17 -r c16859834288 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"),