tuned;

--- 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 {