tuned message -- suppress inlined system information;
authorwenzelm
Fri Jan 04 11:07:39 2013 +0100 (2013-01-04)
changeset 50713dae523e6198b
parent 50712 3e6eb9c4fc6d
child 50714 2af9e4614ba4
tuned message -- suppress inlined system information;
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.scala	Fri Jan 04 01:39:32 2013 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Fri Jan 04 11:07:39 2013 +0100
     1.3 @@ -650,7 +650,8 @@
     1.4                  progress.echo(name + " FAILED")
     1.5                  if (rc != 130) {
     1.6                    progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
     1.7 -                  val tail = out_lines.drop(out_lines.length - 20 max 0)
     1.8 +                  val lines = out_lines.filterNot(_.startsWith("\f"))
     1.9 +                  val tail = lines.drop(lines.length - 20 max 0)
    1.10                    progress.echo("\n" + cat_lines(tail))
    1.11                  }
    1.12