equal
deleted
inserted
replaced
18 object Task_Statistics |
18 object Task_Statistics |
19 { |
19 { |
20 def apply(session_name: String, task_statistics: List[Properties.T]): Task_Statistics = |
20 def apply(session_name: String, task_statistics: List[Properties.T]): Task_Statistics = |
21 new Task_Statistics(session_name, task_statistics) |
21 new Task_Statistics(session_name, task_statistics) |
22 |
22 |
23 def apply(info: Build.Session_Log_Info): Task_Statistics = |
23 def apply(info: Build_Log.Session_Info): Task_Statistics = |
24 apply(info.session_name, info.task_statistics) |
24 apply(info.session_name, info.task_statistics) |
25 } |
25 } |
26 |
26 |
27 final class Task_Statistics private( |
27 final class Task_Statistics private( |
28 val session_name: String, val task_statistics: List[Properties.T]) |
28 val session_name: String, val task_statistics: List[Properties.T]) |