src/Pure/Admin/build_status.scala
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,