# HG changeset patch # User wenzelm # Date 1342637719 -7200 # Node ID 4a8f06cbf8bbb8a5d4bf5d8bbb22da17a9d28715 # Parent 752de4e10162dbe0ee77400f8ae9a45137c4363a tuned import; diff -r 752de4e10162 -r 4a8f06cbf8bb src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Wed Jul 18 20:01:55 2012 +0200 +++ b/src/Pure/General/scan.scala Wed Jul 18 20:55:19 2012 +0200 @@ -12,7 +12,7 @@ import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader} import scala.util.parsing.combinator.RegexParsers -import java.io.{File, InputStream, BufferedInputStream, FileInputStream} +import java.io.{File, BufferedInputStream, FileInputStream} object Scan