changeset 73604 | 51b291ae3e2d |
parent 72763 | 3cc73d00553c |
child 73897 | 0ddb5de0506e |
--- a/src/Pure/ML/ml_process.scala Sun Apr 25 21:12:59 2021 +0200 +++ b/src/Pure/ML/ml_process.scala Sun Apr 25 22:33:15 2021 +0200 @@ -124,7 +124,7 @@ use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args Bash.process( - "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + Bash.strings(bash_args), cwd = cwd, env = env ++ env_options ++ env_tmp ++ env_functions,