src/Pure/Tools/server.scala
changeset 71714 9eb584b1c86a
parent 71713 928fd852f3e2
child 71726 a5fda30edae2
--- a/src/Pure/Tools/server.scala	Mon Apr 06 21:07:38 2020 +0200
+++ b/src/Pure/Tools/server.scala	Mon Apr 06 21:12:11 2020 +0200
@@ -490,7 +490,7 @@
 
       if (operation_list) {
         for {
-          server_info <- using(SQLite.open_database(Data.database))(list(_))
+          server_info <- using(SQLite.open_database(Data.database))(list)
           if server_info.active
         } Output.writeln(server_info.toString, stdout = true)
       }