# HG changeset patch
# User wenzelm
# Date 1457455953 -3600
# Node ID a4ea3a222e0ed17ce023e2a07583ef6197747174
# Parent  c115e69f457f54d5e367e891f6fb09c7ad29f3dd
tuned signature;

diff -r c115e69f457f -r a4ea3a222e0e src/Pure/System/ml_process.scala
--- a/src/Pure/System/ml_process.scala	Tue Mar 08 14:44:11 2016 +0100
+++ b/src/Pure/System/ml_process.scala	Tue Mar 08 17:52:33 2016 +0100
@@ -14,6 +14,7 @@
     args: List[String] = Nil,
     modes: List[String] = Nil,
     secure: Boolean = false,
+    redirect: Boolean = false,
     process_socket: String = ""): Bash.Process =
   {
     val load_heaps =
@@ -77,7 +78,7 @@
       (eval_heaps ::: eval_exit ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
         map(eval => List("--eval", eval)).flatten ::: args
 
-    Bash.process(env = env, script =
+    Bash.process(env = env, redirect = redirect, script =
       """
         [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle