no comment -- File.read_stream already enforces UTF8 (like HTML5) and HTTP servers often produce a wrong charset encoding;
authorwenzelm
Thu, 10 Apr 2014 10:06:54 +0200
changeset 56503 9e23fafe4037
parent 56502 db2836f65d42
child 56504 d71f4be7e287
no comment -- File.read_stream already enforces UTF8 (like HTML5) and HTTP servers often produce a wrong charset encoding;
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 }
   }
 }