src/Pure/General/mercurial.scala
changeset 76883 186e07be32c3
parent 76617 d5adc9126ae8
child 77218 86217697863c
--- 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"