# HG changeset patch
# User wenzelm
# Date 1594892612 -7200
# Node ID efd169aed4dc273a7a105ca4a1320fb22e5a6ca1
# Parent  7b112eedc8598223bf2d38fa2c9003dd0228768b
more robust: avoid potential problems with encoding of directory name;

diff -r 7b112eedc859 -r efd169aed4dc src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Wed Jul 15 20:06:45 2020 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Thu Jul 16 11:43:32 2020 +0200
@@ -42,10 +42,10 @@
       if (props.nonEmpty) consume(props)
     }
 
-    Bash.process("exec \"$POLYML_EXE\" -q --use " +
-      File.bash_platform_path(Path.explode("~~/src/Pure/ML/ml_statistics.ML")) +
-      " --eval " + Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +
-          ML_Syntax.print_double(delay.seconds)))
+    Bash.process("exec \"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
+        Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +
+          ML_Syntax.print_double(delay.seconds)),
+        cwd = Path.explode("~~").file)
       .result(progress_stdout = progress_stdout, strict = false).check
   }