# HG changeset patch
# User wenzelm
# Date 1357294059 -3600
# Node ID dae523e6198bc91b1940bcaef0f5d60e1e27fe5c
# Parent  3e6eb9c4fc6d3285fa1394daf05d85a79137d94a
tuned message -- suppress inlined system information;

diff -r 3e6eb9c4fc6d -r dae523e6198b 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))
                 }