# HG changeset patch # User wenzelm # Date 1457693361 -3600 # Node ID 092c63734cc656811ff150f956c6995634f302ed # Parent 75452e3eda14637c99281a073c01a68b9ae945fa tuned message; diff -r 75452e3eda14 -r 092c63734cc6 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Fri Mar 11 08:39:57 2016 +0100 +++ b/src/Pure/Tools/build.scala Fri Mar 11 11:49:21 2016 +0100 @@ -1102,10 +1102,8 @@ val sessions = getopts(args) val progress = new Console_Progress(verbose) - val start_time = Time.now() - val show_timing = !no_build && verbose - if (show_timing) { + if (verbose) { progress.echo( Library.trim_line( Isabelle_System.bash( @@ -1113,25 +1111,25 @@ progress.echo(show_settings()) } + val start_time = Time.now() val results = progress.interrupt_handler { build_results(options, progress, requirements, all_sessions, build_heap, clean_build, dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files, check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions) } + val elapsed_time = Time.now() - start_time - if (show_timing) { - val elapsed_time = Time.now() - start_time - + if (verbose) { progress.echo( Library.trim_line( Isabelle_System.bash("""echo "Finished at "; date""").out)) + } - val total_timing = - (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _). - copy(elapsed = elapsed_time) - progress.echo(total_timing.message_resources) - } + val total_timing = + (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _). + copy(elapsed = elapsed_time) + progress.echo(total_timing.message_resources) results.rc }