enable multi-builds (again, see also 0c7419d3dd59);
authorwenzelm
Sat, 04 Nov 2023 20:28:07 +0100
changeset 78903 54318ecceec9
parent 78902 6dc989ae4327
child 78904 f6b3d0cf4147
enable multi-builds (again, see also 0c7419d3dd59);
src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Nov 04 20:10:17 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Nov 04 20:28:07 2023 +0100
@@ -177,6 +177,8 @@
     detect: PostgreSQL.Source = "",
     active: () => Boolean = () => true
   ) {
+    def replicate(n: Int): List[Remote_Build] = Library.replicate(n, this)
+
     def open_session(options: Options): SSH.Session =
       SSH.open_session(options, host = host, user = user, port = port)
 
@@ -366,7 +368,7 @@
             " -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" +
             " -e ISABELLE_SWIPL=/usr/local/bin/swipl",
           args = "-a -d '~~/src/Benchmarks'")),
-      List(remote_build_studio1),
+      remote_build_studio1.replicate(2),
       List(
         Remote_Build("macOS, quick_and_dirty", "mini2",
           options = "-m32 -M4 -t quick_and_dirty -p pide_session=false",
@@ -377,7 +379,7 @@
           options = "-m32 -M4 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs",
           detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"),
           active = () => false)),
-      List(remote_build_mini3),
+      remote_build_mini3.replicate(3),
       List(
         Remote_Build("Windows", "vmnipkow9", historic = true, history = 90,
           components_base = "/cygdrive/d/isatest/contrib",