# HG changeset patch
# User wenzelm
# Date 1296650680 -3600
# Node ID 44a2e0db281fa83579f934054cb74ccad0582d09
# Parent  b5d7b15166bf82be530a449c39c5476091917735
tuned comment;

diff -r b5d7b15166bf -r 44a2e0db281f src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Wed Feb 02 13:38:09 2011 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Feb 02 13:44:40 2011 +0100
@@ -159,7 +159,7 @@
 (* queue *)
 
 datatype queue = Queue of
- {groups: task list Inttab.table,   (*groups with presently active members*)
+ {groups: task list Inttab.table,   (*groups with presently known members*)
   jobs: jobs};                      (*job dependency graph*)
 
 fun make_queue groups jobs = Queue {groups = groups, jobs = jobs};