src/Pure/Admin/build_status.scala
changeset 65857 5d29d93766ef
parent 65854 db070951dfee
child 65859 95ddb6dea0d5
     1.1 --- a/src/Pure/Admin/build_status.scala	Wed May 17 21:08:11 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Wed May 17 21:24:16 2017 +0200
     1.3 @@ -169,7 +169,7 @@
     1.4              val ml_stats =
     1.5                ML_Statistics(
     1.6                  if (ml_statistics)
     1.7 -                    store.uncompress_properties(res.bytes(Build_Log.Data.ml_statistics))
     1.8 +                  Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics))
     1.9                  else Nil, heading = session_name + " (Isabelle/ " + isabelle_version + ")")
    1.10  
    1.11              val entry =