diff -r e760242101fc -r e3ccf0809d51 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Fri May 02 19:51:40 2014 +0200 +++ b/src/Pure/System/options.scala Fri May 02 20:01:45 2014 +0200 @@ -147,13 +147,13 @@ val options = (Options.init() /: more_options)(_ + _) if (get_option != "") - System.out.println(options.check_name(get_option).value) + Console.println(options.check_name(get_option).value) if (export_file != "") File.write(Path.explode(export_file), YXML.string_of_body(options.encode)) if (get_option == "" && export_file == "") - System.out.println(options.print) + Console.println(options.print) case _ => error("Bad arguments:\n" + cat_lines(args)) }