# HG changeset patch
# User wenzelm
# Date 1368875050 -7200
# Node ID 4894df243482a4b81af3f3f07291dfe0631aa8c9
# Parent  83b7b88770c9048ca1e4a18860d5c153be32861e
discontinued odd workaround for scala-2.10.0-RC1;

diff -r 83b7b88770c9 -r 4894df243482 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat May 18 13:00:05 2013 +0200
+++ b/src/Pure/Tools/build.scala	Sat May 18 13:04:10 2013 +0200
@@ -894,8 +894,7 @@
     val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
     if (rc != 0 && (verbose || !no_build)) {
       val unfinished =
-        (for ((name, res) <- results.iterator if res.rc != 0) yield name).toList
-          .sorted(scala.math.Ordering.String)  // FIXME scala-2.10.0-RC1
+        (for ((name, res) <- results.iterator if res.rc != 0) yield name).toList.sorted
       progress.echo("Unfinished session(s): " + commas(unfinished))
     }
     rc