src/Pure/System/standard_system.scala
changeset 36015 6111de7c916a
parent 36011 3ff725ac13a4
child 36136 89b1a136edef
     1.1 --- a/src/Pure/System/standard_system.scala	Tue Mar 30 00:12:42 2010 +0200
     1.2 +++ b/src/Pure/System/standard_system.scala	Tue Mar 30 00:13:27 2010 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  object Standard_System
     1.5  {
     1.6    val charset = "UTF-8"
     1.7 -  val codec = Codec(charset)
     1.8 +  def codec(): Codec = Codec(charset)
     1.9  
    1.10  
    1.11    /* permissive UTF-8 decoding */
    1.12 @@ -136,7 +136,7 @@
    1.13    def process_output(proc: Process): (String, Int) =
    1.14    {
    1.15      proc.getOutputStream.close
    1.16 -    val output = Source.fromInputStream(proc.getInputStream)(codec).mkString  // FIXME
    1.17 +    val output = Source.fromInputStream(proc.getInputStream)(codec()).mkString  // FIXME
    1.18      val rc =
    1.19        try { proc.waitFor }
    1.20        finally {