changeset 65778 | 666a1bac126b |
parent 65776 | 373d708898d4 |
child 65780 | 8baf789b1537 |
--- a/src/Pure/General/sql.scala Mon May 08 16:38:11 2017 +0200 +++ b/src/Pure/General/sql.scala Mon May 08 17:16:40 2017 +0200 @@ -133,7 +133,7 @@ if (body == "") error("Missing SQL body for table " + quote(name)) else SQL.enclose(body) - def query_name: Source = query + " AS " + SQL.ident(name) + def query_named: Source = query + " AS " + SQL.ident(name) def create(strict: Boolean = false, sql_type: Type.Value => Source): Source = {