# HG changeset patch
# User wenzelm
# Date 1313674621 -7200
# Node ID b94951f06e48b52fc3c04f73dec566c7da392be6
# Parent  c21ecbb028b6677e4c3ed676559a8db07935b198
export Par_List.managed_results, to enable specific treatment of results apart from default Par_Exn.release_first;

diff -r c21ecbb028b6 -r b94951f06e48 src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Thu Aug 18 15:15:43 2011 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Thu Aug 18 15:37:01 2011 +0200
@@ -16,6 +16,7 @@
 
 signature PAR_LIST =
 sig
+  val managed_results: string -> ('a -> 'b) -> 'a list -> 'b Exn.result list
   val map_name: string -> ('a -> 'b) -> 'a list -> 'b list
   val map: ('a -> 'b) -> 'a list -> 'b list
   val get_some: ('a -> 'b option) -> 'a list -> 'b option