# HG changeset patch
# User wenzelm
# Date 1488300508 -3600
# Node ID 1995b421d8effd4130e68740cd8ec78f7623466a
# Parent  a2522ea4321606ab91c93758e2b73da3bc27a6f6
tuned;

diff -r a2522ea43216 -r 1995b421d8ef src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Tue Feb 28 16:26:05 2017 +0100
+++ b/src/Pure/General/url.scala	Tue Feb 28 17:48:28 2017 +0100
@@ -37,11 +37,8 @@
   /* read */
 
   private def read(url: URL, gzip: Boolean): String =
-  {
-    val stream = url.openStream
-    try { File.read_stream(if (gzip) new GZIPInputStream(stream) else stream) }
-    finally { stream.close }
-  }
+    using(url.openStream)(stream =>
+      File.read_stream(if (gzip) new GZIPInputStream(stream) else stream))
 
   def read(url: URL): String = read(url, false)
   def read_gzip(url: URL): String = read(url, true)