changeset 78193 | 443a443bbe7b |
parent 78191 | 6e52cda26ad4 |
child 78196 | 140a6f2e3728 |
--- 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 {