# HG changeset patch
# User wenzelm
# Date 1350557250 -7200
# Node ID 8a23e8a6bc025f039925e6d91fe29f622a5b4d53
# Parent  c4bd02e32d353843f51f7cb1f5680227c48e28a2
tuned comment;

diff -r c4bd02e32d35 -r 8a23e8a6bc02 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Oct 18 12:26:30 2012 +0200
+++ b/src/Pure/Concurrent/future.ML	Thu Oct 18 12:47:30 2012 +0200
@@ -26,10 +26,10 @@
   * Future tasks are organized in groups, which are block-structured.
     When forking a new new task, the default is to open an individual
     subgroup, unless some common group is specified explicitly.
-    Failure of one group member causes the immediate peers to be
-    interrupted eventually (i.e. none by default).  Interrupted tasks
-    that lack regular result information, will pick up parallel
-    exceptions from the cumulative group context (as Par_Exn).
+    Failure of one group member causes peer and subgroup members to be
+    interrupted eventually.  Interrupted tasks that lack regular
+    result information, will pick up parallel exceptions from the
+    cumulative group context (as Par_Exn).
 
   * Future task groups may be canceled: present and future group
     members will be interrupted eventually.