# HG changeset patch # User wenzelm # Date 1354727252 -3600 # Node ID 11c96cac860d490f611bc3aab670a27c21d5e038 # Parent 9b6f5f758c31c5c825b4cac5267a0b6eccd8222c tuned message; diff -r 9b6f5f758c31 -r 11c96cac860d src/Pure/System/build_dialog.scala --- a/src/Pure/System/build_dialog.scala Wed Dec 05 17:48:58 2012 +0100 +++ b/src/Pure/System/build_dialog.scala Wed Dec 05 18:07:32 2012 +0100 @@ -88,7 +88,7 @@ /* main build */ - progress.echo("Build started ...") + progress.echo("Build started for Isabelle/" + session + " ...") default_thread_pool.submit(() => { val (out, rc) =