diff -r 5539322f68c9 -r 5b3440850d36 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Fri Jul 20 22:39:59 2012 +0200 +++ b/src/Pure/System/options.scala Fri Jul 20 23:16:54 2012 +0200 @@ -51,8 +51,7 @@ def parse_entries(file: JFile): List[Options => Options] = { - val toks = syntax.scan(Standard_System.read_file(file)) - parse_all(rep(entry), Token.reader(toks, file.toString)) match { + parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.toString)) match { case Success(result, _) => result case bad => error(bad.toString) }