diff -r 10f8f12c61b0 -r c3b35f7c8e0e src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Sun Jul 16 09:50:42 2023 +0200 +++ b/src/Pure/General/sql.scala Sun Jul 16 09:54:55 2023 +0200 @@ -325,7 +325,7 @@ def execute(): Boolean = rep.execute() def execute_query(): Result = new Result(this, rep.executeQuery()) - def close(): Unit = rep.close() + override def close(): Unit = rep.close() } @@ -435,7 +435,7 @@ } else None - def close(): Unit = connection.close() + override def close(): Unit = connection.close() def transaction[A](body: => A): A = { val auto_commit = connection.getAutoCommit()