--- a/src/Pure/General/url.scala Fri Dec 30 13:25:29 2022 +0100
+++ b/src/Pure/General/url.scala Fri Dec 30 16:23:32 2022 +0100
@@ -105,10 +105,15 @@
/* generic path notation: local, ssh, rsync, ftp, http */
def append_path(prefix: String, suffix: String): String =
- if (prefix.endsWith(":") || prefix.endsWith("/") || prefix.isEmpty) prefix + suffix
- else if (prefix.endsWith(":.") || prefix.endsWith("/.") || prefix == ".") {
+ if (prefix.endsWith(":") || prefix.endsWith("/") || prefix.endsWith("\\") || prefix.isEmpty) {
+ prefix + suffix
+ }
+ else if (prefix.endsWith(":.") || prefix.endsWith("/.") || prefix.endsWith("\\.") || prefix == ".") {
prefix.substring(0, prefix.length - 1) + suffix
}
+ else if (prefix.contains('\\') || suffix.contains('\\')) {
+ prefix + "\\" + suffix
+ }
else prefix + "/" + suffix
def direct_path(prefix: String): String = append_path(prefix, ".")