src/Pure/General/url.scala

--- a/src/Pure/General/url.scala	Sun Dec 11 12:52:46 2022 +0100
+++ b/src/Pure/General/url.scala	Sun Dec 11 13:46:34 2022 +0100
@@ -102,14 +102,17 @@
   def canonical_file_name(uri: String): String = canonical_file(uri).getPath
 
 
-  /* generic path notation: local, ssh, rsync, http */
+  /* generic path notation: local, ssh, rsync, ftp, http */
 
   def direct_path(prefix: String): String =
-    if (prefix.endsWith(":") || prefix.endsWith("/")) prefix + "."
-    else if (prefix.endsWith(":.") || prefix.endsWith("/.")) prefix
+    if (prefix.endsWith(":") || prefix.endsWith("/") || prefix.isEmpty) prefix + "."
+    else if (prefix.endsWith(":.") || prefix.endsWith("/.") || prefix == ".") prefix
     else prefix + "/."
 
   def append_path(prefix: String, suffix: String): String =
-    if (prefix.endsWith(":") || prefix.endsWith("/")) prefix + suffix
+    if (prefix.endsWith(":") || prefix.endsWith("/") || prefix.isEmpty) prefix + suffix
+    else if (prefix.endsWith(":.") || prefix.endsWith("/.") || prefix == ".") {
+      prefix.substring(0, prefix.length - 1) + suffix
+    }
     else prefix + "/" + suffix
 }