| Thu, 23 Jun 2011 23:12:00 +0200 | wenzelm | more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished! | changeset | files |
| Thu, 23 Jun 2011 23:05:38 +0200 | wenzelm | clarified EXCEPTIONS [] (cf. Exn.is_interrupt and Runtime.exn_message); | changeset | files |
| Thu, 23 Jun 2011 20:30:48 +0200 | wenzelm | more robust concurrent builds; | changeset | files |