tuned;

--- 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 = () =>
         {