# HG changeset patch
# User wenzelm
# Date 1679852160 -7200
# Node ID 6a2daddc238c4561d3660ef788af32dd2297fb34
# Parent  3f4163b83d4f612ae4518d0ff86d9074efd77f13
tuned signature;

diff -r 3f4163b83d4f -r 6a2daddc238c src/Pure/Admin/component_cygwin.scala
--- a/src/Pure/Admin/component_cygwin.scala	Sun Mar 26 19:31:05 2023 +0200
+++ b/src/Pure/Admin/component_cygwin.scala	Sun Mar 26 19:36:00 2023 +0200
@@ -29,7 +29,7 @@
         val cygwin_exe_name = mirror + "/setup-x86_64.exe"
         val cygwin_exe = cygwin_isabelle + Path.explode("cygwin.exe")
         Bytes.write(cygwin_exe,
-          try { Bytes.read(Url(cygwin_exe_name)) }
+          try { Bytes.read_url(cygwin_exe_name) }
           catch { case ERROR(_) => error("Failed to download " + quote(cygwin_exe_name)) })
 
         File.write(cygwin_isabelle + Path.explode("cygwin_mirror"), mirror)
diff -r 3f4163b83d4f -r 6a2daddc238c src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sun Mar 26 19:31:05 2023 +0200
+++ b/src/Pure/General/bytes.scala	Sun Mar 26 19:36:00 2023 +0200
@@ -69,6 +69,8 @@
       new Bytes(out.toByteArray, 0, out.size)
     }
 
+  def read_url(name: String): Bytes = using(Url(name).openStream)(read_stream(_))
+
   def read(file: JFile): Bytes = {
     val length = file.length
     val limit = if (length < 0 || length > Integer.MAX_VALUE) Integer.MAX_VALUE else length.toInt
@@ -77,8 +79,6 @@
 
   def read(path: Path): Bytes = read(path.file)
 
-  def read(url: URL): Bytes = using(url.openStream)(read_stream(_))
-
   def read_slice(path: Path, offset: Long = 0L, limit: Long = Long.MaxValue): Bytes = {
     val start = offset.max(0L)
     val len = (path.file.length - start).max(0L).min(limit)