src/Pure/Build/store.scala
changeset 80123 7e4c3bb3d062
parent 80122 66d7a923b750
child 80128 2fe244c4bb01
--- a/src/Pure/Build/store.scala	Tue Apr 16 16:37:08 2024 +0200
+++ b/src/Pure/Build/store.scala	Tue Apr 16 16:38:54 2024 +0200
@@ -401,9 +401,11 @@
     server: SSH.Server = SSH.no_server,
     progress: Progress = new Progress
   ): Unit = {
-    maybe_using_heaps_database(database_server, server = server) { db =>
-      val slice = Space.MiB(options.real("build_database_slice"))
-      sessions.foreach(ML_Heap.store(db, _, slice, cache = cache.compress, progress = progress))
+    if (sessions.nonEmpty) {
+      maybe_using_heaps_database(database_server, server = server) { db =>
+        val slice = Space.MiB(options.real("build_database_slice"))
+        sessions.foreach(ML_Heap.store(db, _, slice, cache = cache.compress, progress = progress))
+      }
     }
   }