src/Pure/Tools/build.scala
changeset 65278 b553d0edc440
parent 65253 85c0ac5c2589
child 65281 c70e7d24a16d
     1.1 --- a/src/Pure/Tools/build.scala	Thu Mar 16 21:09:13 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Thu Mar 16 21:22:01 2017 +0100
     1.3 @@ -372,7 +372,7 @@
     1.4      if (clean_build) {
     1.5        for (name <- full_tree.graph.all_succs(selected)) {
     1.6          val files =
     1.7 -          List(Path.basic(name), Sessions.log(name), Sessions.log_gz(name)).
     1.8 +          List(Path.basic(name), store.log(name), store.log_gz(name)).
     1.9              map(store.output_dir + _).filter(_.is_file)
    1.10          if (files.nonEmpty) progress.echo("Cleaning " + name + " ...")
    1.11          if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
    1.12 @@ -429,18 +429,18 @@
    1.13                val lines1 = if (tail == 0) lines else lines.drop(lines.length - tail max 0)
    1.14                process_result.copy(
    1.15                  out_lines =
    1.16 -                  "(see also " + (store.output_dir + Sessions.log(name)).file.toString + ")" ::
    1.17 +                  "(see also " + (store.output_dir + store.log(name)).file.toString + ")" ::
    1.18                    lines1)
    1.19              }
    1.20  
    1.21              val heap_stamp =
    1.22                if (process_result.ok) {
    1.23 -                (store.output_dir + Sessions.log(name)).file.delete
    1.24 +                (store.output_dir + store.log(name)).file.delete
    1.25                  val heap_stamp =
    1.26                    for (path <- job.output_path if path.is_file)
    1.27                      yield Sessions.write_heap_digest(path)
    1.28  
    1.29 -                File.write_gzip(store.output_dir + Sessions.log_gz(name),
    1.30 +                File.write_gzip(store.output_dir + store.log_gz(name),
    1.31                    terminate_lines(
    1.32                      session_sources_stamp(name) ::
    1.33                      input_heaps.map(INPUT_HEAP + _) :::
    1.34 @@ -451,9 +451,9 @@
    1.35                }
    1.36                else {
    1.37                  (store.output_dir + Path.basic(name)).file.delete
    1.38 -                (store.output_dir + Sessions.log_gz(name)).file.delete
    1.39 +                (store.output_dir + store.log_gz(name)).file.delete
    1.40  
    1.41 -                File.write(store.output_dir + Sessions.log(name),
    1.42 +                File.write(store.output_dir + store.log(name),
    1.43                    terminate_lines(process_result.out_lines))
    1.44                  progress.echo(name + " FAILED")
    1.45                  if (!process_result.interrupted) progress.echo(process_result_tail.out)