# HG changeset patch # User wenzelm # Date 1677767961 -3600 # Node ID 1082f0d6628bbf9220c024dbae7085faf207200c # Parent abc9706a4ca2da8ef04b8f0468ea146a10870854 tuned; diff -r abc9706a4ca2 -r 1082f0d6628b src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Thu Mar 02 15:39:14 2023 +0100 +++ b/src/Pure/ML/ml_process.scala Thu Mar 02 15:39:21 2023 +0100 @@ -117,9 +117,10 @@ bash_env.put("ISABELLE_TMP", File.standard_path(isabelle_tmp)) bash_env.put("POLYSTATSDIR", isabelle_tmp.getAbsolutePath) - val policy = options.string("ML_process_policy") match { case "" => "" case s => s + " " } + val process_policy = options.string("ML_process_policy") + val process_prefix = if_proper(process_policy, process_policy + " ") - Bash.process(policy + """"$ML_HOME/poly" -q """ + Bash.strings(bash_args), + Bash.process(process_prefix + """"$ML_HOME/poly" -q """ + Bash.strings(bash_args), cwd = cwd, env = bash_env, redirect = redirect,