# HG changeset patch
# User wenzelm
# Date 1457371900 -3600
# Node ID 973b12bccbc5dd8e0d889777293d8754d9f1d0c7
# Parent  8ebffdaf2ce2580690fe24ab3301f43b8717afb0
tuned;

diff -r 8ebffdaf2ce2 -r 973b12bccbc5 src/Pure/System/ml_process.scala
--- a/src/Pure/System/ml_process.scala	Mon Mar 07 18:20:22 2016 +0100
+++ b/src/Pure/System/ml_process.scala	Mon Mar 07 18:31:40 2016 +0100
@@ -78,7 +78,8 @@
       Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
       (eval_heaps ::: eval_exit ::: eval_secure ::: eval_modes ::: eval_options ::: eval_process).
         map(eval => List("--eval", eval)).flatten ::: args
-    val bash_script =
+
+    Bash.process(env = env, script =
       """
         [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
 
@@ -95,8 +96,6 @@
         rmdir "$ISABELLE_TMP"
 
         exit "$RC"
-      """
-
-    Bash.process(bash_script, env = env)
+      """)
   }
 }