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 {