recovered Output.writeln for remote build_history (cf. ed8940d6295c), in order to have log files copied and removed;
authorwenzelm
Mon, 07 Nov 2016 20:05:30 +0100
changeset 64472 c2191352e908
parent 64471 c40c2975fb02
child 64473 6eff987ab718
recovered Output.writeln for remote build_history (cf. ed8940d6295c), in order to have log files copied and removed;
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)
     }