src/Pure/Admin/isabelle_cronjob.scala
changeset 64294 303976a45afe
parent 64277 5ca4ac099e94
child 64295 6aefa7e66888
     1.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 18 07:04:08 2016 +0200
     1.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 18 10:05:38 2016 +0200
     1.3 @@ -97,19 +97,21 @@
     1.4      host: String,
     1.5      user: String = "",
     1.6      port: Int = SSH.default_port,
     1.7 -    shared_home: Boolean = false,
     1.8 +    shared_home: Boolean = true,
     1.9      options: String = "",
    1.10      args: String = "-o timeout=10800 -a")
    1.11  
    1.12    private val remote_builds =
    1.13      List(
    1.14 -      Remote_Build("lxbroy10", options = "-m32 -M4 -N", shared_home = true),
    1.15 +      Remote_Build("lxbroy10", options = "-m32 -M4 -N"),
    1.16        Remote_Build("macbroy2", options = "-m32 -M4"),
    1.17        Remote_Build("macbroy30", options = "-m32 -M2"),
    1.18        Remote_Build("macbroy31", options = "-m32 -M2"))
    1.19  
    1.20    private def remote_build_history(rev: String, r: Remote_Build): Logger_Task =
    1.21 -    Logger_Task("build_history-" + r.host, logger =>
    1.22 +  {
    1.23 +    val task_name = "build_history-" + r.host
    1.24 +    Logger_Task(task_name, logger =>
    1.25        {
    1.26          using(logger.ssh_context.open_session(host = r.host, user = r.user, port = r.port))(
    1.27            ssh =>
    1.28 @@ -120,12 +122,15 @@
    1.29                    isabelle_repos.ext(r.host),
    1.30                    isabelle_repos_source = isabelle_dev_source,
    1.31                    self_update = !r.shared_home,
    1.32 -                  options = r.options + " -f -r " + File.bash_string(rev),
    1.33 +                  options =
    1.34 +                    r.options + " -f -r " + File.bash_string(rev) +
    1.35 +                      " -N " + File.bash_string(task_name),
    1.36                    args = r.args)
    1.37                for ((log, bytes) <- results)
    1.38                  Bytes.write(logger.log_dir + Path.explode(log), bytes)
    1.39              })
    1.40        })
    1.41 +  }
    1.42  
    1.43  
    1.44