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