# HG changeset patch
# User wenzelm
# Date 1457819497 -3600
# Node ID 247963aa1c5d2364bedbd67a6f7fdd743970633a
# Parent  8dac815f9f6a5c8cc013269ef6c1be1483ace9c9
tuned;

diff -r 8dac815f9f6a -r 247963aa1c5d src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Sat Mar 12 22:31:09 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala	Sat Mar 12 22:51:37 2016 +0100
@@ -99,10 +99,7 @@
         map(eval => List("--eval", eval)).flatten ::: args
 
     Bash.process(
-      """
-        librarypath "$ML_HOME"
-        exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """
-      """,
+      """librarypath "$ML_HOME"; exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args),
       cwd = cwd, env = env ++ env_options ++ env_tmp, redirect = redirect,
       cleanup = () =>
         {