src/Pure/General/xz.scala
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
 }