--- 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
}