| changeset 62505 | 9e2a65912111 |
| parent 59180 | c0fa3b3bdabd |
| child 62891 | 7a11ea5c9626 |
--- a/src/Pure/Concurrent/par_list.ML Thu Mar 03 14:03:06 2016 +0100 +++ b/src/Pure/Concurrent/par_list.ML Thu Mar 03 15:23:02 2016 +0100 @@ -46,7 +46,7 @@ val results = restore_attributes Future.join_results futures handle exn => - (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn); + (if Exn.is_interrupt exn then Future.cancel_group group else (); Exn.reraise exn); in results end) (); fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);