tuned;
authorwenzelm
Mon, 06 Apr 2020 21:12:11 +0200
changeset 71714 9eb584b1c86a
parent 71713 928fd852f3e2
child 71715 9e2f52d0aec3
tuned;
src/Pure/Tools/server.scala
--- 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)
       }