--- a/src/Pure/System/options.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/System/options.scala Thu Feb 20 14:36:17 2014 +0100
@@ -140,13 +140,13 @@
val options = (Options.init() /: more_options)(_ + _)
if (get_option != "")
- java.lang.System.out.println(options.check_name(get_option).value)
+ System.out.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 == "")
- java.lang.System.out.println(options.print)
+ System.out.println(options.print)
0
case _ => error("Bad arguments:\n" + cat_lines(args))