| changeset 71961 | af779738a8f9 |
| parent 68018 | 3747fe57eb67 |
| child 73024 | 337e1b135d2f |
--- a/src/Pure/General/xz.scala Fri Jun 19 16:12:32 2020 +0200 +++ b/src/Pure/General/xz.scala Fri Jun 19 18:22:03 2020 +0200 @@ -28,6 +28,7 @@ type Cache = ArrayCache + def no_cache(): ArrayCache = ArrayCache.getDummyCache() def cache(): ArrayCache = ArrayCache.getDefaultCache() def make_cache(): ArrayCache = new BasicArrayCache }