src/Pure/System/getopts.scala
changeset 67178 70576478bda9
parent 62454 38c89353b349
     1.1 --- a/src/Pure/System/getopts.scala	Sun Dec 10 18:43:08 2017 +0100
     1.2 +++ b/src/Pure/System/getopts.scala	Sun Dec 10 20:29:00 2017 +0100
     1.3 @@ -29,7 +29,7 @@
     1.4  {
     1.5    def usage(): Nothing =
     1.6    {
     1.7 -    Console.println(usage_text)
     1.8 +    Output.writeln(usage_text, stdout = true)
     1.9      sys.exit(1)
    1.10    }
    1.11