# HG changeset patch
# User wenzelm
# Date 1762633112 -3600
# Node ID 6ed617560333457258a64f706bfca70ec6501653
# Parent  29cba276be2372abc9778a9cf0b400989767b643
proper platform_path for Windows;

diff -r 29cba276be23 -r 6ed617560333 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),