minor performance tuning: avoid redundant server access;
authorwenzelm
Tue, 16 Apr 2024 16:38:54 +0200
changeset 80123 7e4c3bb3d062
parent 80122 66d7a923b750
child 80124 455ddb251ece
minor performance tuning: avoid redundant server access;
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))
+      }
     }
   }