# HG changeset patch
# User wenzelm
# Date 1478545530 -3600
# Node ID c2191352e908a40f7213d4bcc1089e4433f3a592
# Parent  c40c2975fb02909cd127b1b9aae9c4daef62fa9b
recovered Output.writeln for remote build_history (cf. ed8940d6295c), in order to have log files copied and removed;

diff -r c40c2975fb02 -r c2191352e908 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Mon Nov 07 19:09:10 2016 +0100
+++ b/src/Pure/Admin/build_history.scala	Mon Nov 07 20:05:30 2016 +0100
@@ -354,6 +354,8 @@
           max_heap = max_heap, more_settings = more_settings, verbose = verbose,
           build_tags = build_tags, build_args = build_args)
 
+      for ((_, log_path) <- results) Output.writeln(log_path.implode, stdout = true)
+
       val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc }
       if (rc != 0) sys.exit(rc)
     }