src/Pure/Build/build_schedule.scala
changeset 79892 c793de82db34
parent 79891 d8b4bfe82bb5
child 79895 4ec26ed6f481
equal deleted inserted replaced
79891:d8b4bfe82bb5 79892:c793de82db34
   988               Build_Log.Session_Entry(
   988               Build_Log.Session_Entry(
   989                 chapter = info.chapter,
   989                 chapter = info.chapter,
   990                 groups = info.groups,
   990                 groups = info.groups,
   991                 hostname = Some(result.node_info.hostname),
   991                 hostname = Some(result.node_info.hostname),
   992                 threads = Some(timing_data.host_infos.num_threads(result.node_info)),
   992                 threads = Some(timing_data.host_infos.num_threads(result.node_info)),
       
   993                 start = Some(result.start_date - build_start),
   993                 timing = result.process_result.timing,
   994                 timing = result.process_result.timing,
   994                 sources = Some(result.output_shasum.digest.toString),
   995                 sources = Some(result.output_shasum.digest.toString),
   995                 status = Some(status))
   996                 status = Some(status))
   996             }
   997             }
   997             else
   998             else