# HG changeset patch
# User wenzelm
# Date 1594809816 -7200
# Node ID aa6a36c730c97fbba69fa72f6a7821b14c4ec1da
# Parent  e48a5b6b755465b39ac2a2ca70d2b53da2ad0b87
proper platform path for Windows;

diff -r e48a5b6b7554 -r aa6a36c730c9 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Wed Jul 15 12:30:25 2020 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Wed Jul 15 12:43:36 2020 +0200
@@ -43,7 +43,7 @@
     }
 
     Bash.process("exec \"$POLYML_EXE\" -q --use " +
-      File.bash_path(Path.explode("~~/src/Pure/ML/ml_statistics.ML")) +
+      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)))
       .result(progress_stdout = progress_stdout, strict = false).check