changeset 78986 | 10680bb927cd |
parent 78900 | 9f7a94117666 |
child 78987 | 3fb4dbffca79 |
--- a/src/Pure/Admin/build_status.scala Sat Nov 18 16:58:14 2023 +0100 +++ b/src/Pure/Admin/build_status.scala Sat Nov 18 18:52:34 2023 +0100 @@ -292,7 +292,8 @@ val ml_stats = ML_Statistics( if (ml_statistics) { - Properties.uncompress(res.bytes(Build_Log.private_data.ml_statistics), cache = store.cache) + Properties.uncompress( + res.bytes(Build_Log.private_data.ml_statistics), cache = store.cache) } else Nil, domain = ml_statistics_domain,