author | wenzelm |
Fri, 04 Jan 2013 11:07:39 +0100 | |
changeset 50713 | dae523e6198b |
parent 50712 | 3e6eb9c4fc6d |
child 50714 | 2af9e4614ba4 |
--- a/src/Pure/Tools/build.scala Fri Jan 04 01:39:32 2013 +0100 +++ b/src/Pure/Tools/build.scala Fri Jan 04 11:07:39 2013 +0100 @@ -650,7 +650,8 @@ progress.echo(name + " FAILED") if (rc != 130) { progress.echo("(see also " + (output_dir + log(name)).file.toString + ")") - val tail = out_lines.drop(out_lines.length - 20 max 0) + val lines = out_lines.filterNot(_.startsWith("\f")) + val tail = lines.drop(lines.length - 20 max 0) progress.echo("\n" + cat_lines(tail)) }