| Fri, 04 Feb 2011 20:40:25 +0100 | wenzelm | tuned signature; | file | diff | annotate |
| Fri, 04 Feb 2011 16:33:12 +0100 | wenzelm | Task_Queue.update_timing: more precise treatment of interruptibility; | file | diff | annotate |
| Wed, 02 Feb 2011 20:32:50 +0100 | wenzelm | eliminated slightly odd abstract type Task_Queue.deps; | file | diff | annotate |
| Wed, 02 Feb 2011 17:26:07 +0100 | wenzelm | refined Task_Queue.dequeue_deps (more incremental); | file | diff | annotate |
| Wed, 02 Feb 2011 15:04:09 +0100 | wenzelm | maintain Task_Queue.group within Task_Queue.task; | file | diff | annotate |
| Wed, 02 Feb 2011 13:44:40 +0100 | wenzelm | tuned comment; | file | diff | annotate |
| Wed, 02 Feb 2011 13:38:09 +0100 | wenzelm | Future.join_results: discontinued post-hoc recording of dynamic dependencies; | file | diff | annotate |
| Tue, 01 Feb 2011 22:24:28 +0100 | wenzelm | more informative task timing: some dependency tracking; | file | diff | annotate |