# HG changeset patch
# User wenzelm
# Date 1592583723 -7200
# Node ID af779738a8f93f7829cc50f866951717a468b254
# Parent  6a64205b491a0cf2f7d29f12defd8d7d487104c1
clarified signature;

diff -r 6a64205b491a -r af779738a8f9 src/Pure/General/xz.scala
--- 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
 }