# HG changeset patch
# User wenzelm
# Date 1689494095 -7200
# Node ID c3b35f7c8e0e33da5173d54172fcd4ae7f66f5f3
# Parent  10f8f12c61b080fae5d6bb0f25319608f564f113
tuned;

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()