tuned comment;
authorwenzelm
Wed, 02 Feb 2011 13:44:40 +0100
changeset 41682 44a2e0db281f
parent 41681 b5d7b15166bf
child 41683 73dde8006820
tuned comment;
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};