tuned -- more visible;
authorwenzelm
Fri May 12 14:40:21 2017 +0200 (2017-05-12)
changeset 658060156222f2a18
parent 65805 d3c5898f1a5e
child 65807 a830c6257393
tuned -- more visible;
src/Pure/Admin/isabelle_cronjob.scala
     1.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Fri May 12 14:33:57 2017 +0200
     1.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri May 12 14:40:21 2017 +0200
     1.3 @@ -138,7 +138,17 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  private val remote_builds: List[List[Remote_Build]] =
     1.8 +  val remote_builds_old: List[Remote_Build] =
     1.9 +    List(
    1.10 +      Remote_Build("Poly/ML test", "lxbroy8",
    1.11 +        options = "-m32 -B -M1x2,2 -t polyml-test -e 'init_component /home/isabelle/contrib/polyml-5.7-20170217'",
    1.12 +        args = "-N -g timing",
    1.13 +        detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test")),
    1.14 +      Remote_Build("Mac OS X 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a",
    1.15 +        detect = Build_Log.Prop.build_start + " < date '2017-03-03'"))
    1.16 +
    1.17 +
    1.18 +  val remote_builds: List[List[Remote_Build]] =
    1.19    {
    1.20      List(
    1.21        List(Remote_Build("Poly/ML 5.7 Linux", "lxbroy8",
    1.22 @@ -171,16 +181,6 @@
    1.23            detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))))
    1.24    }
    1.25  
    1.26 -  private val remote_builds_old: List[Remote_Build] =
    1.27 -    List(
    1.28 -      Remote_Build("Poly/ML test", "lxbroy8",
    1.29 -        options = "-m32 -B -M1x2,2 -t polyml-test -e 'init_component /home/isabelle/contrib/polyml-5.7-20170217'",
    1.30 -        args = "-N -g timing",
    1.31 -        detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test")),
    1.32 -      Remote_Build("Mac OS X 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a",
    1.33 -        detect = Build_Log.Prop.build_start + " < date '2017-03-03'"))
    1.34 -
    1.35 -                      
    1.36    private def remote_build_history(rev: String, r: Remote_Build): Logger_Task =
    1.37    {
    1.38      val task_name = "build_history-" + r.host