# HG changeset patch
# User wenzelm
# Date 1713278334 -7200
# Node ID 7e4c3bb3d0626f6ea246c559268c7ea1a5127f48
# Parent  66d7a923b750b86351697cda4cdc25865bb151c4
minor performance tuning: avoid redundant server access;

diff -r 66d7a923b750 -r 7e4c3bb3d062 src/Pure/Build/store.scala
--- 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))
+      }
     }
   }