# HG changeset patch
# User wenzelm
# Date 1494007253 -7200
# Node ID 4eab1aa8f9c3baa2f5c359472321bc096ccb531c
# Parent  03257db12a04edc84e2066f61f5ad43c7f9a57c8
tuned;

diff -r 03257db12a04 -r 4eab1aa8f9c3 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Fri May 05 18:35:30 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri May 05 20:00:53 2017 +0200
@@ -97,13 +97,12 @@
     detect: SQL.Source = "")
   {
     def sql: SQL.Source =
-      SQL.enclose(
-        Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
-        Build_Log.Prop.build_host + " = " + SQL.string(host)) +
-        (if (detect == "") "" else " AND " + SQL.enclose(detect))
+      Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
+      Build_Log.Prop.build_host + " = " + SQL.string(host) +
+      (if (detect == "") "" else " AND " + SQL.enclose(detect))
   }
 
-  val remote_builds =
+  val remote_builds: List[List[Remote_Build]] =
   {
     List(
       List(Remote_Build("polyml-test", "lxbroy8",