diff -r d27d1224c67f -r 7c57d9586f4c src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -59,7 +59,7 @@
     }
 
     val env_prefix =
-      if (stats_dir.isEmpty) "" else "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n"
+      if_proper(stats_dir, "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n")
 
     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) + " " +