# HG changeset patch
# User wenzelm
# Date 1677768920 -3600
# Node ID 10147ecf9196593538a2841c1ca77325bd9d72ba
# Parent  1e10689ee184a593e8fc38918bb04c43034cf53d
tuned, following ML_Statistics.monitor;

diff -r 1e10689ee184 -r 10147ecf9196 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Thu Mar 02 15:51:24 2023 +0100
+++ b/src/Pure/ML/ml_process.scala	Thu Mar 02 15:55:20 2023 +0100
@@ -120,7 +120,7 @@
     val process_policy = options.string("ML_process_policy")
     val process_prefix = if_proper(process_policy, process_policy + " ")
 
-    Bash.process(process_prefix + """"$ML_HOME/poly" -q """ + Bash.strings(bash_args),
+    Bash.process(process_prefix + "\"$POLYML_EXE\" -q " + Bash.strings(bash_args),
       cwd = cwd,
       env = bash_env,
       redirect = redirect,