src/Pure/General/url.scala
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 }
   }
 }