do not store bulky ml_statistics;
authorwenzelm
Wed May 17 23:13:56 2017 +0200 (2017-05-17)
changeset 65861f35abc25d7b1
parent 65860 ce6be2e40d47
child 65862 5441c51a2d38
child 65869 a6ed757b8585
do not store bulky ml_statistics;
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Wed May 17 23:05:30 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Wed May 17 23:13:56 2017 +0200
     1.3 @@ -98,8 +98,7 @@
     1.4      ml_timing: Timing,
     1.5      maximum_heap: Long,
     1.6      average_heap: Long,
     1.7 -    final_heap: Long,
     1.8 -    ml_statistics: ML_Statistics)
     1.9 +    final_heap: Long)
    1.10  
    1.11    def read_data(options: Options,
    1.12      progress: Progress = No_Progress,
    1.13 @@ -197,8 +196,7 @@
    1.14                      Build_Log.Data.ml_timing_gc),
    1.15                  maximum_heap = ml_stats.maximum_heap_size,
    1.16                  average_heap = ml_stats.average_heap_size,
    1.17 -                final_heap = res.long(Build_Log.Data.heap_size),
    1.18 -                ml_statistics = ml_stats)
    1.19 +                final_heap = res.long(Build_Log.Data.heap_size))
    1.20  
    1.21              val sessions = data_entries.getOrElse(data_name, Map.empty)
    1.22              val entries = sessions.get(session_name).map(_.entries) getOrElse Nil