equal
deleted
inserted
replaced
511 } |
511 } |
512 else { |
512 else { |
513 (output_dir + log_gz(name)).file.delete |
513 (output_dir + log_gz(name)).file.delete |
514 File.write(output_dir + log(name), out) |
514 File.write(output_dir + log(name), out) |
515 echo(name + " FAILED") |
515 echo(name + " FAILED") |
516 echo("(see also " + log(name).file.toString + ")") |
516 echo("(see also " + (output_dir + log(name)).file.toString + ")") |
517 val lines = split_lines(out) |
517 val lines = split_lines(out) |
518 val tail = lines.drop(lines.length - 20 max 0) |
518 val tail = lines.drop(lines.length - 20 max 0) |
519 echo("\n" + cat_lines(tail)) |
519 echo("\n" + cat_lines(tail)) |
520 } |
520 } |
521 loop(pending - name, running - name, results + (name -> (false, rc))) |
521 loop(pending - name, running - name, results + (name -> (false, rc))) |