# HG changeset patch # User wenzelm # Date 1343128310 -7200 # Node ID 8f10b1f6c992a4f837c894f54a1cde13b9e19892 # Parent 6ebb6cdd36a5965af719a4688cd55e9323b70c40 tuned message; diff -r 6ebb6cdd36a5 -r 8f10b1f6c992 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Tue Jul 24 12:54:34 2012 +0200 +++ b/src/Pure/System/build.scala Tue Jul 24 13:11:50 2012 +0200 @@ -474,7 +474,13 @@ else { sleep(); loop(pending, running, results) } } - (0 /: loop(queue, Map.empty, Map.empty))({ case (rc1, (_, rc2)) => rc1 max rc2 }) + val results = loop(queue, Map.empty, Map.empty) + val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 }) + if (rc != 0) { + val unfinished = (for ((name, r) <- results.iterator if r != 0) yield name).toList.sorted + echo("Unfinished session(s): " + commas(unfinished)) + } + rc }