# HG changeset patch
# User wenzelm
# Date 1495055636 -7200
# Node ID f35abc25d7b1b301b0b450394dfcc4503884c17f
# Parent  ce6be2e40d47512b87cea1af3280d2981beabc3b
do not store bulky ml_statistics;

diff -r ce6be2e40d47 -r f35abc25d7b1 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Wed May 17 23:05:30 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Wed May 17 23:13:56 2017 +0200
@@ -98,8 +98,7 @@
     ml_timing: Timing,
     maximum_heap: Long,
     average_heap: Long,
-    final_heap: Long,
-    ml_statistics: ML_Statistics)
+    final_heap: Long)
 
   def read_data(options: Options,
     progress: Progress = No_Progress,
@@ -197,8 +196,7 @@
                     Build_Log.Data.ml_timing_gc),
                 maximum_heap = ml_stats.maximum_heap_size,
                 average_heap = ml_stats.average_heap_size,
-                final_heap = res.long(Build_Log.Data.heap_size),
-                ml_statistics = ml_stats)
+                final_heap = res.long(Build_Log.Data.heap_size))
 
             val sessions = data_entries.getOrElse(data_name, Map.empty)
             val entries = sessions.get(session_name).map(_.entries) getOrElse Nil