diff -r c537905c2125 -r 9d9b30741fc4 src/Pure/Tools/server.scala --- a/src/Pure/Tools/server.scala Mon Mar 06 15:12:37 2023 +0100 +++ b/src/Pure/Tools/server.scala Mon Mar 06 15:38:50 2023 +0100 @@ -410,12 +410,12 @@ val server_info = Info(name, server.port, server.password) db.execute_statement(Data.table.delete(sql = Data.name.where_equal(name))) - db.using_statement(Data.table.insert()) { stmt => - stmt.string(1) = server_info.name - stmt.int(2) = server_info.port - stmt.string(3) = server_info.password - stmt.execute() - } + db.execute_statement(Data.table.insert(), body = + { stmt => + stmt.string(1) = server_info.name + stmt.int(2) = server_info.port + stmt.string(3) = server_info.password + }) server.start() (server_info, Some(server))