changeset 73416 | 08aa4c1ed579 |
parent 73367 | 77ef8bef0593 |
child 73417 | 1dcc2b228b8b |
--- a/src/Pure/General/url.scala Fri Mar 12 19:43:49 2021 +0100 +++ b/src/Pure/General/url.scala Fri Mar 12 19:46:37 2021 +0100 @@ -80,13 +80,6 @@ def read(name: String): String = read(Url(name), false) def read_gzip(name: String): String = read(Url(name), true) - def read_bytes(url: URL): Bytes = - { - val connection = url.openConnection - val length = connection.getContentLength - using(connection.getInputStream)(Bytes.read_stream(_, hint = length)) - } - /* file URIs */