# HG changeset patch
# User wenzelm
# Date 1495742393 -7200
# Node ID de3adcf6a276acc00817ba78d05c0db7cd482c1d
# Parent  38eb5d633b0bfedcc8e7370bc1db0a30bafa88cd
prefer strict result (in contrast to 0f3b0a929c02);

diff -r 38eb5d633b0b -r de3adcf6a276 src/Pure/Admin/build_history.scala
--- 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)
+      }
     })
   }
 }
diff -r 38eb5d633b0b -r de3adcf6a276 src/Pure/Admin/isabelle_cronjob.scala
--- 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),