src/Pure/General/sql.scala
changeset 78266 d8c99a497502
parent 78264 c8fde312c895
child 78270 0bd366fad888
--- a/src/Pure/General/sql.scala	Fri Jul 07 18:04:45 2023 +0200
+++ b/src/Pure/General/sql.scala	Sat Jul 08 13:13:10 2023 +0200
@@ -259,7 +259,7 @@
       if (synchronized) db.synchronized { run } else run
     }
 
-    def make_table(name: String, columns: List[Column], body: String = ""): Table = {
+    def make_table(columns: List[Column], body: String = "", name: String = ""): Table = {
       val table_name =
         List(proper_string(table_prefix), proper_string(name)).flatten.mkString("_")
       require(table_name.nonEmpty, "Undefined database table name")