# 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