# HG changeset patch # User wenzelm # Date 1672483864 -3600 # Node ID b8e1c31580126d7379c6ea74132e0e96c2203885 # Parent 893eeef9ef08a2052d2a70a74ebd9b3cc52ea1a0 tuned comments; diff -r 893eeef9ef08 -r b8e1c3158012 src/Pure/General/url.scala --- a/src/Pure/General/url.scala Sat Dec 31 11:48:32 2022 +0100 +++ b/src/Pure/General/url.scala Sat Dec 31 11:51:04 2022 +0100 @@ -102,7 +102,7 @@ def canonical_file_name(uri: String): String = canonical_file(uri).getPath - /* generic path notation: local, ssh, rsync, ftp, http */ + /* generic path notation: standard, platform, ssh, rsync, ftp, http */ private val separators1 = "/\\" private val separators2 = ":/\\"