# HG changeset patch
# User wenzelm
# Date 1687436945 -7200
# Node ID 443a443bbe7bb12c929e27a7f390d2bc87cec6da
# Parent  752a7751b3d32274428bc7c105644329205b0612
tuned;

diff -r 752a7751b3d3 -r 443a443bbe7b src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Wed Jun 21 15:56:48 2023 +0200
+++ b/src/Pure/ML/ml_heap.scala	Thu Jun 22 14:29:05 2023 +0200
@@ -115,7 +115,7 @@
     database: Option[SQL.Database],
     heap: Path,
     slice: Long,
-    cache: Compress.Cache = Compress.Cache.none,
+    cache: Compress.Cache = Compress.Cache.none
   ): SHA1.Digest = {
     val digest = write_file_digest(heap)
     database match {