| changeset 56503 | 9e23fafe4037 | 
| parent 56501 | 5fda9e5c5874 | 
| child 62248 | dca0bac351b2 | 
--- 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 } } }