src/Pure/Tools/server.scala
changeset 77541 9d9b30741fc4
parent 77540 c537905c2125
child 77552 080422b3d914
--- 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))