# HG changeset patch
# User wenzelm
# Date 1478945970 -3600
# Node ID 234571db1b90d307a95eb04172238e0e0cfc2117
# Parent  159ea1055b393dfcf286f2e73e068ef0ca7e663f
tuned output;

diff -r 159ea1055b39 -r 234571db1b90 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Sat Nov 12 10:29:01 2016 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Sat Nov 12 11:19:30 2016 +0100
@@ -83,10 +83,11 @@
 
     /* bash */
 
-    def bash(cwd: Path, script: String, echo: Boolean = false): Process_Result =
+    def bash(cwd: Path, script: String, redirect: Boolean = false, echo: Boolean = false)
+        : Process_Result =
       progress.bash(
         if (other_bash == "") script else Bash.string(other_bash) + " -c " + Bash.string(script),
-        cwd = cwd.file, echo = echo)
+        cwd = cwd.file, redirect = redirect, echo = echo)
 
 
     /* configure and make */
@@ -105,7 +106,7 @@
           rm -rf target
           make compiler && make compiler && make install
         } || { echo "Build failed" >&2; exit 2; }
-      """, echo = true).check
+      """, redirect = true, echo = true).check
 
     val ldd_files =
       if (Platform.is_linux) {
@@ -121,7 +122,7 @@
     val sha1_files =
       if (sha1_root.isDefined) {
         val dir1 = sha1_root.get
-        bash(dir1, "./build " + platform, echo = true).check
+        bash(dir1, "./build " + platform, redirect = true, echo = true).check
         val dir2 = dir1 + Path.explode(platform)
         File.read_dir(dir2).map(entry => dir2.implode + "/" + entry)
       }