do not store bulky ml_statistics;
authorwenzelm
Wed, 17 May 2017 23:13:56 +0200
changeset 65861 f35abc25d7b1
parent 65860 ce6be2e40d47
child 65862 a6ed757b8585
child 65863 5441c51a2d38
do not store bulky ml_statistics;
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