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