src/Pure/ML/ml_process.scala
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,