proper platform_path for Windows;
authorwenzelm
Sat, 08 Nov 2025 21:18:32 +0100
changeset 83534 6ed617560333
parent 83533 29cba276be23
child 83535 c2d0eadf32e6
proper platform_path for Windows;
src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Sat Nov 08 20:16:08 2025 +0100
+++ b/src/Pure/ML/ml_process.scala	Sat Nov 08 21:18:32 2025 +0100
@@ -157,7 +157,7 @@
       "C:" -> (arg => cwd = Path.explode(arg)),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
-      "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
+      "f:" -> (arg => eval_args = eval_args ::: List("--use", File.platform_path(arg))),
       "l:" -> (arg => logic = arg),
       "m:" -> (arg => modes = arg :: modes),
       "o:" -> (arg => options = options + arg),