--- a/src/Pure/Admin/build_status.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/Admin/build_status.scala Sat Jan 02 22:22:34 2021 +0100
@@ -286,8 +286,7 @@
val ml_stats =
ML_Statistics(
if (ml_statistics) {
- Properties.uncompress(
- res.bytes(Build_Log.Data.ml_statistics), cache = store.xz_cache)
+ Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics), cache = store.cache)
}
else Nil,
domain = ml_statistics_domain,
@@ -320,8 +319,8 @@
stored_heap = ML_Statistics.mem_scale(res.long(Build_Log.Data.heap_size)),
status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)),
errors =
- Build_Log.uncompress_errors(res.bytes(Build_Log.Data.errors),
- cache = store.xz_cache))
+ Build_Log.uncompress_errors(
+ res.bytes(Build_Log.Data.errors), cache = store.cache.xz))
val sessions = data_entries.getOrElse(data_name, Map.empty)
val session =