# HG changeset patch
# User wenzelm
# Date 1361379884 -3600
# Node ID 6e40d0bb89e399c7d4fc8d22591aaa1b40564acf
# Parent  dff3471dd8bcc84da69e471a1b456fc32485c2bd
prefer outdegree in comparison again (cf. 88c96e836ed6) -- NB: big jobs might hide behind small ones in this naive queuing scheme;

diff -r dff3471dd8bc -r 6e40d0bb89e3 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Feb 20 15:22:22 2013 +0100
+++ b/src/Pure/Tools/build.scala	Wed Feb 20 18:04:44 2013 +0100
@@ -313,9 +313,9 @@
         }
 
         def compare(name1: String, name2: String): Int =
-          compare_timing(name2, name1) match {
+          outdegree(name2) compare outdegree(name1) match {
             case 0 =>
-              outdegree(name2) compare outdegree(name1) match {
+              compare_timing(name2, name1) match {
                 case 0 =>
                   timeout(name2) compare timeout(name1) match {
                     case 0 => name1 compare name2