src/Pure/Tools/build.scala
changeset 68220 8fc4e3d1df86
parent 68219 c0341c0080e2
child 68221 dbef88c2b6c5
     1.1 --- a/src/Pure/Tools/build.scala	Sat May 19 15:45:45 2018 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Sat May 19 16:13:39 2018 +0200
     1.3 @@ -467,19 +467,13 @@
     1.4  
     1.5      store.prepare_output_dir()
     1.6  
     1.7 -    // cleanup
     1.8 -    def cleanup(name: String, echo: Boolean = false)
     1.9 -    {
    1.10 -      val files =
    1.11 -        List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
    1.12 -          map(store.output_dir + _).filter(_.is_file)
    1.13 -      if (files.nonEmpty) progress.echo_if(echo, "Cleaning " + name + " ...")
    1.14 -      val res = files.map(p => p.file.delete)
    1.15 -      if (!res.forall(ok => ok)) progress.echo_if(echo, name + " FAILED to delete")
    1.16 -    }
    1.17      if (clean_build) {
    1.18        for (name <- full_sessions.build_descendants(full_sessions.build_selection(selection1))) {
    1.19 -        cleanup(name, echo = true)
    1.20 +        val (relevant, ok) = store.clean_output(name)
    1.21 +        if (relevant) {
    1.22 +          if (ok) progress.echo("Cleaned " + name)
    1.23 +          else progress.echo(name + " FAILED to clean")
    1.24 +        }
    1.25        }
    1.26      }
    1.27  
    1.28 @@ -618,7 +612,7 @@
    1.29                  else if (ancestor_results.forall(_.ok) && !progress.stopped) {
    1.30                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
    1.31  
    1.32 -                  cleanup(name)
    1.33 +                  store.clean_output(name)
    1.34                    using(store.open_output_database(name))(store.init_session_info(_, name))
    1.35  
    1.36                    val numa_node = numa_nodes.next(used_node(_))