changeset 78375 | 234f2ff9afe6 |
parent 78187 | 2df0f3604a67 |
child 78396 | 7853d9072d1b |
--- a/src/Pure/Tools/server.scala Mon Jul 17 11:39:32 2023 +0200 +++ b/src/Pure/Tools/server.scala Mon Jul 17 12:15:06 2023 +0200 @@ -375,7 +375,7 @@ } def list(db: SQLite.Database): List[Info] = - if (db.tables.contains(Data.table.name)) { + if (db.exists_table(Data.table)) { db.execute_query_statement(Data.table.select(), List.from[Info], { res =>