# HG changeset patch
# User wenzelm
# Date 1476350547 -7200
# Node ID 68e95e5b2b7d178006e4336c1674aa2290a8a506
# Parent  c69a77e0124a770bdd8a9099602e1014dd207e47
tuned;

diff -r c69a77e0124a -r 68e95e5b2b7d src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 11:22:12 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 11:22:27 2016 +0200
@@ -145,20 +145,25 @@
     File.write(main_state_file, main_start_date + " " + log_service.hostname)
 
 
-    /* parallel tasks */
+    /* manage tasks */
+
+    def sequential_tasks(tasks: List[Logger_Task])
+    {
+      tasks.map(task => log_service.run_task(Date.now(), task))
+    }
 
     def parallel_tasks(tasks: List[Logger_Task])
     {
-      @tailrec def await(running: List[Task])
+      @tailrec def join(running: List[Task])
       {
         running.partition(_.is_finished) match {
           case (Nil, Nil) =>
-          case (Nil, _ :: _) => Thread.sleep(500); await(running)
-          case (_ :: _, remaining) => await(remaining)
+          case (Nil, _ :: _) => Thread.sleep(500); join(running)
+          case (_ :: _, remaining) => join(remaining)
         }
       }
       val start_date = Date.now()
-      await(tasks.map(task => log_service.fork_task(start_date, task)))
+      join(tasks.map(task => log_service.fork_task(start_date, task)))
     }