# HG changeset patch
# User wenzelm
# Date 1670764569 -3600
# Node ID 7785ad9114167e1b3e0d84cfd3f0cea06ae8783a
# Parent  7af197063e2f57ce53942655ea64f98f9f0b7d97
tuned: less redundant implementation;

diff -r 7af197063e2f -r 7785ad911416 src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Sun Dec 11 14:10:32 2022 +0100
+++ b/src/Pure/General/url.scala	Sun Dec 11 14:16:09 2022 +0100
@@ -104,15 +104,12 @@
 
   /* generic path notation: local, ssh, rsync, ftp, http */
 
-  def direct_path(prefix: String): String =
-    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.isEmpty) prefix + suffix
     else if (prefix.endsWith(":.") || prefix.endsWith("/.") || prefix == ".") {
       prefix.substring(0, prefix.length - 1) + suffix
     }
     else prefix + "/" + suffix
+
+  def direct_path(prefix: String): String = append_path(prefix, ".")
 }