src/Pure/Tools/server.scala
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 =>