avoid lxbroy7, which is presently inaccessible, but retain its build history in db queries;
authorwenzelm
Tue, 14 Nov 2017 21:16:57 +0100
changeset 67075 eada9bd5fff2
parent 67074 5da20135f560
child 67077 8fa951baba0d
avoid lxbroy7, which is presently inaccessible, but retain its build history in db queries;
src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Nov 14 20:12:47 2017 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Nov 14 21:16:57 2017 +0100
@@ -122,11 +122,12 @@
     args: String = "",
     afp: Boolean = false,
     slow: Boolean = false,
+    more_hosts: List[String] = Nil,
     detect: SQL.Source = "")
   {
     def sql: SQL.Source =
       Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
-      Build_Log.Prop.build_host + " = " + SQL.string(host) +
+      SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts) +
       (if (detect == "") "" else " AND " + SQL.enclose(detect))
 
     def profile: Build_Status.Profile =
@@ -242,9 +243,9 @@
           detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))),
     ) :::
     {
-      for { (host, n) <- List("lxbroy6" -> 1, "lxbroy7" -> 2) }
+      for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy7")) }
       yield {
-        List(Remote_Build("AFP", host = host,
+        List(Remote_Build("AFP", host = hosts.head, more_hosts = hosts.tail,
           options = "-m32 -M1x2 -t AFP -P" + n,
           args = "-N -X slow",
           afp = true,