# HG changeset patch
# User wenzelm
# Date 1397117214 -7200
# Node ID 9e23fafe4037d4567427690fce4771f158c8cce6
# Parent  db2836f65d429924eb32d835c6a78ff1ed37838f
no comment -- File.read_stream already enforces UTF8 (like HTML5) and HTTP servers often produce a wrong charset encoding;

diff -r db2836f65d42 -r 9e23fafe4037 src/Pure/General/url.scala
--- 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 }
   }
 }