# HG changeset patch
# User wenzelm
# Date 1476565667 -7200
# Node ID c1b5165b73dbebbc84d7dfa07f7feec932e43aaf
# Parent  358f9ff08681fd6dabd44782499cf0cbb3be0be0
tuned;

diff -r 358f9ff08681 -r c1b5165b73db src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 15 22:45:27 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 15 23:07:47 2016 +0200
@@ -225,8 +225,7 @@
 
     /* log service */
 
-    val ssh_context = SSH.init(Options.init())
-    val log_service = new Log_Service(progress, ssh_context)
+    val log_service = new Log_Service(progress, SSH.init(Options.init()))
 
     def run(start_date: Date, task: Logger_Task) { log_service.run_task(start_date, task) }