author | wenzelm |
Sat, 31 Dec 2022 11:51:04 +0100 | |
changeset 76841 | b8e1c3158012 |
parent 76840 | 893eeef9ef08 |
child 76842 | 18465808e61f |
--- 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 = ":/\\"