prefer strict result (in contrast to 0f3b0a929c02);
authorwenzelm
Thu, 25 May 2017 21:59:53 +0200
changeset 65929 de3adcf6a276
parent 65928 38eb5d633b0b
child 65930 9a28fc03c3fe
prefer strict result (in contrast to 0f3b0a929c02);
src/Pure/Admin/build_history.scala
src/Pure/Admin/isabelle_cronjob.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)
+      }
     })
   }
 }
--- 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),