src/Pure/System/build.scala
changeset 48473 8f10b1f6c992
parent 48471 9d5ce7f1002d
child 48478 146090de0474
equal deleted inserted replaced
48472:6ebb6cdd36a5 48473:8f10b1f6c992
   472         }
   472         }
   473       }
   473       }
   474       else { sleep(); loop(pending, running, results) }
   474       else { sleep(); loop(pending, running, results) }
   475     }
   475     }
   476 
   476 
   477     (0 /: loop(queue, Map.empty, Map.empty))({ case (rc1, (_, rc2)) => rc1 max rc2 })
   477     val results = loop(queue, Map.empty, Map.empty)
       
   478     val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
       
   479     if (rc != 0) {
       
   480       val unfinished = (for ((name, r) <- results.iterator if r != 0) yield name).toList.sorted
       
   481       echo("Unfinished session(s): " + commas(unfinished))
       
   482     }
       
   483     rc
   478   }
   484   }
   479 
   485 
   480 
   486 
   481   /* command line entry point */
   487   /* command line entry point */
   482 
   488