equal
deleted
inserted
replaced
53 finalized = finalized, |
53 finalized = finalized, |
54 forks = forks, |
54 forks = forks, |
55 runs = runs) |
55 runs = runs) |
56 } |
56 } |
57 |
57 |
58 val empty = make(Iterator.empty) |
58 val empty: Command_Status = make(Iterator.empty) |
59 |
59 |
60 def merge(status_iterator: Iterator[Command_Status]): Command_Status = |
60 def merge(status_iterator: Iterator[Command_Status]): Command_Status = |
61 if (status_iterator.hasNext) { |
61 if (status_iterator.hasNext) { |
62 val status0 = status_iterator.next |
62 val status0 = status_iterator.next |
63 (status0 /: status_iterator)(_ + _) |
63 (status0 /: status_iterator)(_ + _) |