--- a/src/Pure/Admin/build_history.scala Thu May 25 21:55:17 2017 +0200
+++ b/src/Pure/Admin/build_history.scala Thu May 25 21:59:53 2017 +0200
@@ -410,7 +410,7 @@
push_isabelle_home: Boolean = false,
progress: Progress = No_Progress,
options: String = "",
- args: String = ""): (List[(String, Bytes)], Process_Result) =
+ args: String = ""): List[(String, Bytes)] =
{
val isabelle_admin = isabelle_repos_self + Path.explode("Admin")
@@ -455,26 +455,22 @@
{
val output_file = tmp_dir + Path.explode("output")
- val process_result =
- ssh.execute(
- Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
- ssh.bash_path(isabelle_admin + Path.explode("build_history")) +
- " -o " + ssh.bash_path(output_file) + " " + options + " " +
- ssh.bash_path(isabelle_repos_other) + " " + args,
- progress_stdout = progress.echo(_),
- progress_stderr = progress.echo(_),
- strict = false)
+ ssh.execute(
+ Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
+ ssh.bash_path(isabelle_admin + Path.explode("build_history")) +
+ " -o " + ssh.bash_path(output_file) + " " + options + " " +
+ ssh.bash_path(isabelle_repos_other) + " " + args,
+ progress_stdout = progress.echo(_),
+ progress_stderr = progress.echo(_),
+ strict = false).check
- val result =
- for (line <- split_lines(ssh.read(output_file)))
- yield {
- val log = Path.explode(line)
- val bytes = ssh.read_bytes(log)
- ssh.rm(log)
- (log.base.implode, bytes)
- }
-
- (result, process_result)
+ for (line <- split_lines(ssh.read(output_file)))
+ yield {
+ val log = Path.explode(line)
+ val bytes = ssh.read_bytes(log)
+ ssh.rm(log)
+ (log.base.implode, bytes)
+ }
})
}
}
--- a/src/Pure/Admin/isabelle_cronjob.scala Thu May 25 21:55:17 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Thu May 25 21:59:53 2017 +0200
@@ -230,7 +230,7 @@
val self_update = !r.shared_home
val push_isabelle_home = self_update && Mercurial.is_repository(Path.explode("~~"))
- val (results, _) =
+ val results =
Build_History.remote_build_history(ssh,
isabelle_repos,
isabelle_repos.ext(r.host),