diff -r d9913b41a7bc -r 186e07be32c3 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Tue Jan 03 15:32:54 2023 +0100
+++ b/src/Pure/General/mercurial.scala	Tue Jan 03 15:42:25 2023 +0100
@@ -53,7 +53,7 @@
       root + (if (raw) "/raw-rev/" else "/rev/") + rev
 
     def file(path: Path, rev: String = "tip", raw: Boolean = false): String =
-      root + (if (raw) "/raw-file/" else "/file/") + rev + "/" + path.expand.implode
+      root + (if (raw) "/raw-file/" else "/file/") + rev + "/" + File.standard_path(path)
 
     def archive(rev: String = "tip"): String =
       root + "/archive/" + rev + ".tar.gz"