changeset 44247 | 270366301bd7 |
parent 44185 | 05641edb5d30 |
child 44549 | 5e5e6ad3922c |
--- a/src/Pure/ROOT.ML Wed Aug 17 20:08:36 2011 +0200 +++ b/src/Pure/ROOT.ML Wed Aug 17 22:14:22 2011 +0200 @@ -77,7 +77,7 @@ then use "Concurrent/bash.ML" else use "Concurrent/bash_sequential.ML"; -use "Concurrent/mailbox.ML"; +use "Concurrent/par_exn.ML"; use "Concurrent/task_queue.ML"; use "Concurrent/future.ML"; @@ -89,6 +89,7 @@ if Multithreading.available then () else use "Concurrent/par_list_sequential.ML"; +use "Concurrent/mailbox.ML"; use "Concurrent/cache.ML";