# HG changeset patch
# User wenzelm
# Date 1477561198 -7200
# Node ID 0f3b0a929c02074abc9e81d2188d49968891e0e6
# Parent  c0d5e78eb6471847921a4466cbbb538c6e6d3e11
more permissive remote_build_history: failure happens routinely and should not lead error, without saving logs;

diff -r c0d5e78eb647 -r 0f3b0a929c02 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Wed Oct 26 22:40:28 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Thu Oct 27 11:39:58 2016 +0200
@@ -379,7 +379,7 @@
     progress: Progress = Ignore_Progress,
     progress_result: (String, Bytes) => Unit = (log_name: String, bytes: Bytes) => (),
     options: String = "",
-    args: String = ""): List[(String, Bytes)] =
+    args: String = ""): (List[(String, Bytes)], Process_Result) =
   {
     val isabelle_admin = isabelle_repos_self + Path.explode("Admin")
 
@@ -428,12 +428,13 @@
       result += res
     }
 
-    ssh.execute(
-      ssh.bash_path(isabelle_admin + Path.explode("build_history")) + " " + options + " " +
-        ssh.bash_path(isabelle_repos_other) + " " + args,
-      progress_stdout = progress_stdout _,
-      progress_stderr = progress.echo(_)).check
+    val process_result =
+      ssh.execute(
+        ssh.bash_path(isabelle_admin + Path.explode("build_history")) + " " + options + " " +
+          ssh.bash_path(isabelle_repos_other) + " " + args,
+        progress_stdout = progress_stdout _,
+        progress_stderr = progress.echo(_))
 
-    result.toList
+    (result.toList, process_result)
   }
 }