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)
       }