# HG changeset patch
# User wenzelm
# Date 1476954278 -7200
# Node ID e48e2532ac171f5a885b461ae35b24f3c7910672
# Parent  93de02f9c2d9121a98f91c4b60417e8e53e81e01
proper echo;
tuned;

diff -r 93de02f9c2d9 -r e48e2532ac17 src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Thu Oct 20 10:30:11 2016 +0200
+++ b/src/Pure/Admin/other_isabelle.scala	Thu Oct 20 11:04:38 2016 +0200
@@ -7,7 +7,7 @@
 package isabelle
 
 
-private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String)
+class Other_Isabelle(progress: Progress, val isabelle_home: Path, val isabelle_identifier: String)
 {
   other_isabelle =>
 
@@ -17,7 +17,7 @@
   def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
     progress.bash(
       "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" + script,
-      env = null, cwd = isabelle_home.file, redirect = redirect)
+      env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo)
 
   def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
     bash("bin/isabelle " + cmdline, redirect, echo)