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 results = |
120 def progress_result(log_name: String, bytes: Bytes): Unit = |
121 Build_History.remote_build_history(ssh, |
121 Bytes.write(logger.log_dir + Path.explode(log_name), bytes) |
122 isabelle_repos, |
122 |
123 isabelle_repos.ext(r.host), |
123 Build_History.remote_build_history(ssh, |
124 isabelle_repos_source = isabelle_dev_source, |
124 isabelle_repos, |
125 self_update = !r.shared_home, |
125 isabelle_repos.ext(r.host), |
126 options = |
126 isabelle_repos_source = isabelle_dev_source, |
127 r.options + " -f -r " + Bash.string(rev) + " -N " + Bash.string(task_name), |
127 self_update = !r.shared_home, |
128 args = "-o timeout=10800 " + r.args) |
128 progress_result = progress_result _, |
129 for ((log, bytes) <- results) |
129 options = |
130 Bytes.write(logger.log_dir + Path.explode(log), bytes) |
130 r.options + " -f -r " + Bash.string(rev) + " -N " + Bash.string(task_name), |
|
131 args = "-o timeout=10800 " + r.args) |
131 }) |
132 }) |
132 }) |
133 }) |
133 } |
134 } |
134 |
135 |
135 |
136 |