src/Pure/System/options.scala
changeset 56831 e3ccf0809d51
parent 56631 89269bb8e7ca
child 58868 c5e1cce7ace3
     1.1 --- a/src/Pure/System/options.scala	Fri May 02 19:51:40 2014 +0200
     1.2 +++ b/src/Pure/System/options.scala	Fri May 02 20:01:45 2014 +0200
     1.3 @@ -147,13 +147,13 @@
     1.4            val options = (Options.init() /: more_options)(_ + _)
     1.5  
     1.6            if (get_option != "")
     1.7 -            System.out.println(options.check_name(get_option).value)
     1.8 +            Console.println(options.check_name(get_option).value)
     1.9  
    1.10            if (export_file != "")
    1.11              File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
    1.12  
    1.13            if (get_option == "" && export_file == "")
    1.14 -            System.out.println(options.print)
    1.15 +            Console.println(options.print)
    1.16  
    1.17          case _ => error("Bad arguments:\n" + cat_lines(args))
    1.18        }