# HG changeset patch # User wenzelm # Date 1510690617 -3600 # Node ID eada9bd5fff2982c4b41f1767d5dfc1a047e52f4 # Parent 5da20135f56018827ae18effd4b5f3f001c3c4a8 avoid lxbroy7, which is presently inaccessible, but retain its build history in db queries; diff -r 5da20135f560 -r eada9bd5fff2 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,