# HG changeset patch
# User wenzelm
# Date 1672413812 -3600
# Node ID a150dd0ebdd31b61a3aa50e2dade01762e0e5f99
# Parent  eb3b946bdeffc710521242ba322cc7acd165578d
more flexible: implicit support for Windows;

diff -r eb3b946bdeff -r a150dd0ebdd3 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, ".")