| changeset 76354 | 908433a347d1 |
| parent 75393 | 87ebf5a50283 |
| child 76617 | d5adc9126ae8 |
--- a/src/Pure/General/url.scala Fri Oct 21 18:06:32 2022 +0200 +++ b/src/Pure/General/url.scala Fri Oct 21 19:05:48 2022 +0200 @@ -64,8 +64,8 @@ /* strings */ - def decode(s: String): String = URLDecoder.decode(s, UTF8.charset_name) - def encode(s: String): String = URLEncoder.encode(s, UTF8.charset_name) + def decode(s: String): String = URLDecoder.decode(s, UTF8.charset) + def encode(s: String): String = URLEncoder.encode(s, UTF8.charset) /* read */