author | wenzelm |
Sat, 18 Nov 2023 18:52:34 +0100 | |
changeset 78986 | 10680bb927cd |
parent 78985 | 24e686fe043e |
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,