| Wed, 01 Oct 2008 12:00:02 +0200 | wenzelm | more robust treatment of Interrupt (cf. exn.ML); | changeset | files |
| Wed, 01 Oct 2008 12:00:01 +0200 | wenzelm | removed release_results (cf. Exn.release_all, Exn.release_first); | changeset | files |
| Wed, 01 Oct 2008 12:00:00 +0200 | wenzelm | more precise join_futures, improved termination; | changeset | files |