src/Pure/General/url.scala

--- 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, ".")