src/Pure/System/standard_system.scala
changeset 36011 3ff725ac13a4
parent 34300 3f2e25dc99ab
child 36015 6111de7c916a
     1.1 --- a/src/Pure/System/standard_system.scala	Mon Mar 29 01:07:01 2010 -0700
     1.2 +++ b/src/Pure/System/standard_system.scala	Mon Mar 29 22:43:56 2010 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
     1.5    File, FileFilter, IOException}
     1.6  
     1.7 -import scala.io.Source
     1.8 +import scala.io.{Source, Codec}
     1.9  import scala.util.matching.Regex
    1.10  import scala.collection.mutable
    1.11  
    1.12 @@ -20,6 +20,7 @@
    1.13  object Standard_System
    1.14  {
    1.15    val charset = "UTF-8"
    1.16 +  val codec = Codec(charset)
    1.17  
    1.18  
    1.19    /* permissive UTF-8 decoding */
    1.20 @@ -135,7 +136,7 @@
    1.21    def process_output(proc: Process): (String, Int) =
    1.22    {
    1.23      proc.getOutputStream.close
    1.24 -    val output = Source.fromInputStream(proc.getInputStream, charset).mkString  // FIXME
    1.25 +    val output = Source.fromInputStream(proc.getInputStream)(codec).mkString  // FIXME
    1.26      val rc =
    1.27        try { proc.waitFor }
    1.28        finally {