changeset 72849 | c83883da98d6 |
parent 72848 | d5d0e36eda16 |
child 72853 | d0038b553e0e |
--- 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)