# HG changeset patch
# User wenzelm
# Date 1700329954 -3600
# Node ID 10680bb927cd40fe75fc6aca4eb2ebc4eeec8329
# Parent  24e686fe043ed9e9d25e54a49e3f0bfb9b245f1e
tuned whitespace;

diff -r 24e686fe043e -r 10680bb927cd src/Pure/Admin/build_status.scala
--- 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,