| changeset 48277 | f14e564fca1a |
| parent 48027 | 69ba790960ba |
| child 48359 | e544dbcdf097 |
--- a/src/Pure/System/standard_system.scala Tue Jul 17 15:56:19 2012 +0200 +++ b/src/Pure/System/standard_system.scala Tue Jul 17 16:54:23 2012 +0200 @@ -16,7 +16,7 @@ File, FileFilter, IOException} import java.nio.charset.Charset -import scala.io.{Source, Codec} +import scala.io.Codec import scala.util.matching.Regex import scala.collection.mutable