diff -r 2c704ae04db1 -r 014dbbe5331f src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Sun Apr 30 16:32:58 2017 +0200 +++ b/src/Pure/Admin/build_history.scala Sun Apr 30 16:47:30 2017 +0200 @@ -202,8 +202,9 @@ Build_Log.log_filename(Build_History.engine, build_history_date, List(build_host, ml_platform, "M" + threads) ::: build_tags) - val build_info = - Build_Log.Log_File(log_path.base.implode, build_result.out_lines).parse_build_info() + val build_info: Build_Log.Build_Info = + Build_Log.Log_File(log_path.base.implode, build_result.out_lines). + parse_build_info(ml_statistics = true) /* output log */