src/Pure/Tools/server.scala
changeset 67178 70576478bda9
parent 66929 c19b17b72777
child 67784 543e36ae489c
     1.1 --- a/src/Pure/Tools/server.scala	Sun Dec 10 18:43:08 2017 +0100
     1.2 +++ b/src/Pure/Tools/server.scala	Sun Dec 10 20:29:00 2017 +0100
     1.3 @@ -134,11 +134,11 @@
     1.4  
     1.5        if (operation_list) {
     1.6          for (entry <- using(SQLite.open_database(Data.database))(list(_)) if entry.active)
     1.7 -          Console.println(entry.print)
     1.8 +          Output.writeln(entry.print, stdout = true)
     1.9        }
    1.10        else {
    1.11          val (entry, thread) = start(name, port)
    1.12 -        Console.println(entry.print)
    1.13 +        Output.writeln(entry.print, stdout = true)
    1.14          thread.foreach(_.join)
    1.15        }
    1.16      })