suppress inlined properties from log output;
authorwenzelm
Fri Mar 17 21:18:49 2017 +0100 (2017-03-17)
changeset 6529469100bf4ead4
parent 65293 a53a5ae88205
child 65295 5e4e7aaa4270
suppress inlined properties from log output;
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.scala	Fri Mar 17 20:57:20 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Fri Mar 17 21:18:49 2017 +0100
     1.3 @@ -386,15 +386,14 @@
     1.4              if (process_result.ok)
     1.5                progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
     1.6  
     1.7 +            val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
     1.8              val process_result_tail =
     1.9              {
    1.10 -              val lines = process_result.out_lines.filterNot(_.startsWith("\f"))
    1.11                val tail = job.info.options.int("process_output_tail")
    1.12 -              val lines1 = if (tail == 0) lines else lines.drop(lines.length - tail max 0)
    1.13                process_result.copy(
    1.14                  out_lines =
    1.15                    "(see also " + (store.output_dir + store.log(name)).file.toString + ")" ::
    1.16 -                  lines1)
    1.17 +                  (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
    1.18              }
    1.19  
    1.20              val heap_stamp =
    1.21 @@ -404,8 +403,7 @@
    1.22                    for (path <- job.output_path if path.is_file)
    1.23                      yield Sessions.write_heap_digest(path)
    1.24  
    1.25 -                File.write_gzip(store.output_dir + store.log_gz(name),
    1.26 -                  terminate_lines(process_result.out_lines))
    1.27 +                File.write_gzip(store.output_dir + store.log_gz(name), terminate_lines(log_lines))
    1.28  
    1.29                  heap_stamp
    1.30                }
    1.31 @@ -413,8 +411,7 @@
    1.32                  (store.output_dir + Path.basic(name)).file.delete
    1.33                  (store.output_dir + store.log_gz(name)).file.delete
    1.34  
    1.35 -                File.write(store.output_dir + store.log(name),
    1.36 -                  terminate_lines(process_result.out_lines))
    1.37 +                File.write(store.output_dir + store.log(name), terminate_lines(log_lines))
    1.38                  progress.echo(name + " FAILED")
    1.39                  if (!process_result.interrupted) progress.echo(process_result_tail.out)
    1.40