diff -r 3cc075052033 -r d5ef492dd673 src/Pure/ML/ml_statistics.scala --- a/src/Pure/ML/ml_statistics.scala Wed Apr 09 17:40:27 2025 +0200 +++ b/src/Pure/ML/ml_statistics.scala Wed Apr 09 22:23:59 2025 +0200 @@ -57,8 +57,7 @@ if (props.nonEmpty) consume(props) } - val env_prefix = - if_proper(stats_dir, "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n") + val env_prefix = if_proper(stats_dir, Bash.exports("POLYSTATSDIR=" + stats_dir)) Bash.process(env_prefix + "\"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " + Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +