399 sessions: List[Store.Session], |
399 sessions: List[Store.Session], |
400 database_server: Option[SQL.Database], |
400 database_server: Option[SQL.Database], |
401 server: SSH.Server = SSH.no_server, |
401 server: SSH.Server = SSH.no_server, |
402 progress: Progress = new Progress |
402 progress: Progress = new Progress |
403 ): Unit = { |
403 ): Unit = { |
404 maybe_using_heaps_database(database_server, server = server) { db => |
404 if (sessions.nonEmpty) { |
405 val slice = Space.MiB(options.real("build_database_slice")) |
405 maybe_using_heaps_database(database_server, server = server) { db => |
406 sessions.foreach(ML_Heap.store(db, _, slice, cache = cache.compress, progress = progress)) |
406 val slice = Space.MiB(options.real("build_database_slice")) |
|
407 sessions.foreach(ML_Heap.store(db, _, slice, cache = cache.compress, progress = progress)) |
|
408 } |
407 } |
409 } |
408 } |
410 } |
409 |
411 |
410 def open_build_database(path: Path, server: SSH.Server = SSH.no_server): SQL.Database = |
412 def open_build_database(path: Path, server: SSH.Server = SSH.no_server): SQL.Database = |
411 if (build_database_server || build_cluster) open_database_server(server = server) |
413 if (build_database_server || build_cluster) open_database_server(server = server) |