tuned signature;
authorwenzelm
Tue, 08 Mar 2016 17:52:33 +0100
changeset 62557 a4ea3a222e0e
parent 62556 c115e69f457f
child 62558 c46418f12ee1
tuned signature;
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