tuned message -- suppress inlined system information;
authorwenzelm
Fri, 04 Jan 2013 11:07:39 +0100
changeset 50713 dae523e6198b
parent 50712 3e6eb9c4fc6d
child 50714 2af9e4614ba4
tuned message -- suppress inlined system information;
src/Pure/Tools/build.scala
--- 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))
                 }