115 Logger_Task(task_name, logger => |
115 Logger_Task(task_name, logger => |
116 { |
116 { |
117 using(logger.ssh_context.open_session(host = r.host, user = r.user, port = r.port))( |
117 using(logger.ssh_context.open_session(host = r.host, user = r.user, port = r.port))( |
118 ssh => |
118 ssh => |
119 { |
119 { |
|
120 val self_update = !r.shared_home |
|
121 val push_isabelle_home = self_update && Mercurial.is_repository(Path.explode("~~")) |
|
122 |
120 def progress_result(log_name: String, bytes: Bytes): Unit = |
123 def progress_result(log_name: String, bytes: Bytes): Unit = |
121 Bytes.write(logger.log_dir + Path.explode(log_name), bytes) |
124 Bytes.write(logger.log_dir + Path.explode(log_name), bytes) |
122 |
125 |
123 Build_History.remote_build_history(ssh, |
126 Build_History.remote_build_history(ssh, |
124 isabelle_repos, |
127 isabelle_repos, |
125 isabelle_repos.ext(r.host), |
128 isabelle_repos.ext(r.host), |
126 isabelle_repos_source = isabelle_dev_source, |
129 isabelle_repos_source = isabelle_dev_source, |
127 self_update = !r.shared_home, |
130 self_update = self_update, |
|
131 push_isabelle_home = push_isabelle_home, |
128 progress_result = progress_result _, |
132 progress_result = progress_result _, |
129 options = |
133 options = |
130 r.options + " -f -r " + Bash.string(rev) + " -N " + Bash.string(task_name), |
134 r.options + " -f -r " + Bash.string(rev) + " -N " + Bash.string(task_name), |
131 args = "-o timeout=10800 " + r.args) |
135 args = "-o timeout=10800 " + r.args) |
132 }) |
136 }) |