# HG changeset patch
# User wenzelm
# Date 1680978392 -7200
# Node ID f5aca3ed1adb626e3575bec4108262b5a1e17dab
# Parent  4c4bd44ff683e5cf7dad69852722f4af07b7f0ac
tuned comments;

diff -r 4c4bd44ff683 -r f5aca3ed1adb src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Sat Apr 08 20:21:30 2023 +0200
+++ b/src/Pure/General/url.scala	Sat Apr 08 20:26:32 2023 +0200
@@ -102,7 +102,7 @@
   def canonical_file_name(uri: String): String = canonical_file(uri).getPath
 
 
-  /* generic path notation: standard, platform, ssh, rsync, ftp, http */
+  /* generic path notation: standard, platform, ssh, rsync, ftp, http, https */
 
   private val separators1 = "/\\"
   private val separators2 = ":/\\"