prefer outdegree in comparison again (cf. 88c96e836ed6) -- NB: big jobs might hide behind small ones in this naive queuing scheme;
1.1 --- a/src/Pure/Tools/build.scala Wed Feb 20 15:22:22 2013 +0100
1.2 +++ b/src/Pure/Tools/build.scala Wed Feb 20 18:04:44 2013 +0100
1.3 @@ -313,9 +313,9 @@
1.4 }
1.5
1.6 def compare(name1: String, name2: String): Int =
1.7 - compare_timing(name2, name1) match {
1.8 + outdegree(name2) compare outdegree(name1) match {
1.9 case 0 =>
1.10 - outdegree(name2) compare outdegree(name1) match {
1.11 + compare_timing(name2, name1) match {
1.12 case 0 =>
1.13 timeout(name2) compare timeout(name1) match {
1.14 case 0 => name1 compare name2