src/Pure/System/options.scala
changeset 67178 70576478bda9
parent 67004 af72fa58f71b
child 67845 46fa8c2c142a
     1.1 --- a/src/Pure/System/options.scala	Sun Dec 10 18:43:08 2017 +0100
     1.2 +++ b/src/Pure/System/options.scala	Sun Dec 10 20:29:00 2017 +0100
     1.3 @@ -185,13 +185,13 @@
     1.4      }
     1.5  
     1.6      if (get_option != "")
     1.7 -      Console.println(options.check_name(get_option).value)
     1.8 +      Output.writeln(options.check_name(get_option).value, stdout = true)
     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 -      Console.println(options.print)
    1.15 +      Output.writeln(options.print, stdout = true)
    1.16    })
    1.17  }
    1.18