src/Pure/Admin/build_history.scala
changeset 64419 0f3b0a929c02
parent 64376 68ace7f3d78f
child 64453 075c077a6e29
--- 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)
   }
 }