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