author | wenzelm |
Thu, 10 Apr 2014 10:06:54 +0200 | |
changeset 56503 | 9e23fafe4037 |
parent 56502 | db2836f65d42 |
child 56504 | d71f4be7e287 |
--- a/src/Pure/General/url.scala Wed Apr 09 23:22:58 2014 +0200 +++ b/src/Pure/General/url.scala Thu Apr 10 10:06:54 2014 +0200 @@ -29,7 +29,7 @@ def read(name: String): String = { val stream = Url(name).openStream - try { File.read_stream(stream) } // FIXME proper text encoding!? + try { File.read_stream(stream) } finally { stream.close } } }