# HG changeset patch
# User wenzelm
# Date 1220550312 -7200
# Node ID 1179b32f885dc39f62810a9e6c8826e919f2aacb
# Parent  218252dfd81e4d7dfb85bcbd0f3d69cefb90d9d7
added Concurrent/mailbox.ML;

diff -r 218252dfd81e -r 1179b32f885d src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Thu Sep 04 17:24:18 2008 +0200
+++ b/src/Pure/IsaMakefile	Thu Sep 04 19:45:12 2008 +0200
@@ -23,7 +23,8 @@
 
 Pure: $(OUT)/Pure
 
-$(OUT)/Pure: Concurrent/schedule.ML General/ROOT.ML General/alist.ML	\
+$(OUT)/Pure: Concurrent/mailbox.ML Concurrent/receiver.ML		\
+  Concurrent/schedule.ML General/ROOT.ML General/alist.ML		\
   General/balanced_tree.ML General/basics.ML General/buffer.ML		\
   General/file.ML General/graph.ML General/heap.ML General/integer.ML	\
   General/markup.ML General/name_space.ML General/ord_list.ML		\
diff -r 218252dfd81e -r 1179b32f885d src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Sep 04 17:24:18 2008 +0200
+++ b/src/Pure/ROOT.ML	Thu Sep 04 19:45:12 2008 +0200
@@ -23,6 +23,7 @@
 cd "General"; use "ROOT.ML"; cd "..";
 
 (*concurrency within the ML runtime*)
+use "Concurrent/mailbox.ML";
 use "Concurrent/schedule.ML";
 
 (*fundamental structures*)