src/Pure/Tools/build.scala
changeset 50713 dae523e6198b
parent 50707 5b2bf7611662
child 50715 8cfd585b9162
--- 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))
                 }