src/Pure/System/build.scala
changeset 48350 09bf3b73e446
parent 48349 a78e5d399599
child 48351 a0b95a762abb
equal deleted inserted replaced
48349:a78e5d399599 48350:09bf3b73e446
    24     object Key
    24     object Key
    25     {
    25     {
    26       object Ordering extends scala.math.Ordering[Key]
    26       object Ordering extends scala.math.Ordering[Key]
    27       {
    27       {
    28         def compare(key1: Key, key2: Key): Int =
    28         def compare(key1: Key, key2: Key): Int =
    29           key2.order compare key1.order match {
    29           key1.order compare key2.order match {
    30             case 0 => key1.name compare key2.name
    30             case 0 => key1.name compare key2.name
    31             case ord => ord
    31             case ord => ord
    32           }
    32           }
    33       }
    33       }
    34     }
    34     }