# HG changeset patch
# User wenzelm
# Date 1607374977 -3600
# Node ID c83883da98d6b299e80145f46f2070b181a6fc2f
# Parent  d5d0e36eda16ec06b63632c15c2210745345de66
tuned;

diff -r d5d0e36eda16 -r c83883da98d6 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Mon Dec 07 21:49:39 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Mon Dec 07 22:02:57 2020 +0100
@@ -139,7 +139,7 @@
       }
 
       val export_consumer =
-        Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache)
+        Export.consumer(store.open_database(session_name, output = true), store.xz_cache)
 
       val stdout = new StringBuilder(1000)
       val stderr = new StringBuilder(1000)