src/Pure/Concurrent/task_queue.ML
Mon, 08 Jul 2013 12:00:45 +0200 wenzelm allow worker guest threads, which participate actively in future joins, but are outside thread accounting;
less more (0) -30 -10 -1 tip