src/Pure/Tools/build.scala
changeset 72019 940195fbb282
parent 72018 5c9984820caa
child 72021 664e90313a54
equal deleted inserted replaced
72018:5c9984820caa 72019:940195fbb282
   679                     process_result.rc)))
   679                     process_result.rc)))
   680 
   680 
   681             // messages
   681             // messages
   682             process_result.err_lines.foreach(progress.echo)
   682             process_result.err_lines.foreach(progress.echo)
   683 
   683 
       
   684             if (verbose) progress.echo(session_timing(session_name, build_log.session_timing))
       
   685 
   684             if (process_result.ok) {
   686             if (process_result.ok) {
   685               progress.echo(session_finished(session_name, process_result.timing))
   687               progress.echo(session_finished(session_name, process_result.timing))
   686             }
   688             }
   687             else {
   689             else {
   688               progress.echo(session_name + " FAILED")
   690               progress.echo(session_name + " FAILED")