# HG changeset patch
# User wenzelm
# Date 1494944893 -7200
# Node ID aa6e58dc54d02937f785981ccdc292d96c22d659
# Parent  b8ff6314925654efa441b0616c6d6760feb6a819
prefer explicit output file: potentially more robust than stdout;

diff -r b8ff63149256 -r aa6e58dc54d0 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Tue May 16 16:04:50 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Tue May 16 16:28:13 2017 +0200
@@ -441,23 +441,29 @@
 
     /* Admin/build_history */
 
-    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.echo(_),
-        progress_stderr = progress.echo(_),
-        strict = false)
+    ssh.with_tmp_dir(tmp_dir =>
+    {
+      val output_file = tmp_dir + Path.explode("output")
 
-    val result =
-      for (line <- process_result.out_lines)
-      yield {
-        val log = Path.explode(line)
-        val bytes = ssh.read_bytes(log)
-        ssh.rm(log)
-        (log.base.implode, bytes)
-      }
+      val process_result =
+        ssh.execute(
+          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)
 
-    (result, process_result)
+      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)
+    })
   }
 }