src/Pure/Tools/build.scala
changeset 68734 c14a2cc9b5ef
parent 68731 c2dcb7f7a3ef
child 68928 835e5d45359c
equal deleted inserted replaced
68733:76e339ef60e3 68734:c14a2cc9b5ef
   490     val queue = Queue(progress, deps.sessions_structure, store)
   490     val queue = Queue(progress, deps.sessions_structure, store)
   491 
   491 
   492     store.prepare_output_dir()
   492     store.prepare_output_dir()
   493 
   493 
   494     if (clean_build) {
   494     if (clean_build) {
   495       for (name <- full_sessions.build_descendants(full_sessions.build_selection(selection1))) {
   495       for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection1))) {
   496         val (relevant, ok) = store.clean_output(name)
   496         val (relevant, ok) = store.clean_output(name)
   497         if (relevant) {
   497         if (relevant) {
   498           if (ok) progress.echo("Cleaned " + name)
   498           if (ok) progress.echo("Cleaned " + name)
   499           else progress.echo(name + " FAILED to clean")
   499           else progress.echo(name + " FAILED to clean")
   500         }
   500         }