# HG changeset patch
# User wenzelm
# Date 1220555526 -7200
# Node ID a74a1c58036054d2564706648993ba0032b4dcda
# Parent  831e545c655e6c9fe230ecc5f071ddd84858b566
proper header;

diff -r 831e545c655e -r a74a1c580360 src/Pure/Concurrent/mailbox.ML
--- a/src/Pure/Concurrent/mailbox.ML	Thu Sep 04 21:02:42 2008 +0200
+++ b/src/Pure/Concurrent/mailbox.ML	Thu Sep 04 21:12:06 2008 +0200
@@ -1,5 +1,6 @@
 (*  Title:      Pure/Concurrent/mailbox.ML
     ID:         $Id$
+    Author:     Makarius
 
 Concurrent message exchange via mailbox -- with unbounded queueing.
 *)
diff -r 831e545c655e -r a74a1c580360 src/Pure/Concurrent/schedule.ML
--- a/src/Pure/Concurrent/schedule.ML	Thu Sep 04 21:02:42 2008 +0200
+++ b/src/Pure/Concurrent/schedule.ML	Thu Sep 04 21:12:06 2008 +0200
@@ -1,5 +1,6 @@
 (*  Title:      Pure/Concurrent/schedule.ML
     ID:         $Id$
+    Author:     Makarius
 
 Scheduling -- multiple threads working on a queue of tasks.
 *)