src/Pure/Admin/build_status.scala
changeset 73033 d2690444c00a
parent 73031 f93f0597f4fb
child 73120 c3589f2dff31
equal deleted inserted replaced
73032:72b13af7f266 73033:d2690444c00a
   318                 average_heap = ml_stats.average(ML_Statistics.HEAP_SIZE).toLong,
   318                 average_heap = ml_stats.average(ML_Statistics.HEAP_SIZE).toLong,
   319                 stored_heap = ML_Statistics.mem_scale(res.long(Build_Log.Data.heap_size)),
   319                 stored_heap = ML_Statistics.mem_scale(res.long(Build_Log.Data.heap_size)),
   320                 status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)),
   320                 status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)),
   321                 errors =
   321                 errors =
   322                   Build_Log.uncompress_errors(
   322                   Build_Log.uncompress_errors(
   323                     res.bytes(Build_Log.Data.errors), cache = store.cache.xz))
   323                     res.bytes(Build_Log.Data.errors), cache = store.cache))
   324 
   324 
   325             val sessions = data_entries.getOrElse(data_name, Map.empty)
   325             val sessions = data_entries.getOrElse(data_name, Map.empty)
   326             val session =
   326             val session =
   327               sessions.get(session_name) match {
   327               sessions.get(session_name) match {
   328                 case None =>
   328                 case None =>