# HG changeset patch
# User wenzelm
# Date 1708603258 -3600
# Node ID 909031707ff49d54741e6ab50558ba87b83a15cd
# Parent  3f307faf9111e948404e58e4e6a8173fe15d1747
proper store.cache.compress;

diff -r 3f307faf9111 -r 909031707ff4 src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Thu Feb 22 12:57:42 2024 +0100
+++ b/src/Pure/Build/build_job.scala	Thu Feb 22 13:00:58 2024 +0100
@@ -524,7 +524,8 @@
             heaps_database =>
               for (db <- database_server orElse heaps_database) {
                 val slice = Space.MiB(options.real("build_database_slice"))
-                ML_Heap.store(db, store_session, slice, progress = progress)
+                ML_Heap.store(db, store_session, slice,
+                  cache = store.cache.compress, progress = progress)
               }
           }