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