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