equal
deleted
inserted
replaced
486 { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _) |
486 { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _) |
487 def ok: Boolean = rc == 0 |
487 def ok: Boolean = rc == 0 |
488 |
488 |
489 override def toString: String = rc.toString |
489 override def toString: String = rc.toString |
490 } |
490 } |
|
491 |
|
492 def session_finished(session_name: String, timing: Timing): String = |
|
493 "Finished " + session_name + " (" + timing.message_resources + ")" |
|
494 |
|
495 def session_timing(session_name: String, threads: Int, timing: Timing): String = |
|
496 "Timing " + session_name + " (" + threads + " threads, " + timing.message_resources + ")" |
491 |
497 |
492 def build( |
498 def build( |
493 options: Options, |
499 options: Options, |
494 selection: Sessions.Selection = Sessions.Selection.empty, |
500 selection: Sessions.Selection = Sessions.Selection.empty, |
495 progress: Progress = new Progress, |
501 progress: Progress = new Progress, |
676 } |
682 } |
677 |
683 |
678 // messages |
684 // messages |
679 process_result.err_lines.foreach(progress.echo) |
685 process_result.err_lines.foreach(progress.echo) |
680 |
686 |
681 if (process_result.ok) |
687 if (process_result.ok) { |
682 progress.echo( |
688 progress.echo(session_finished(session_name, process_result.timing)) |
683 "Finished " + session_name + " (" + process_result.timing.message_resources + ")") |
689 } |
684 else { |
690 else { |
685 progress.echo(session_name + " FAILED") |
691 progress.echo(session_name + " FAILED") |
686 if (!process_result.interrupted) progress.echo(process_result_tail.out) |
692 if (!process_result.interrupted) progress.echo(process_result_tail.out) |
687 } |
693 } |
688 |
694 |