# HG changeset patch
# User wenzelm
# Date 1689588972 -7200
# Node ID 36a3a9a8b5fe0322b460787176b26e75bd781e57
# Parent  234f2ff9afe65478525e54d48fab99cb588eeff4
more complete check;

diff -r 234f2ff9afe6 -r 36a3a9a8b5fe src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Mon Jul 17 12:15:06 2023 +0200
+++ b/src/Pure/Thy/store.scala	Mon Jul 17 12:16:12 2023 +0200
@@ -150,7 +150,7 @@
       Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = cache)
 
     def read_build(db: SQL.Database, name: String): Option[Store.Build_Info] = {
-      if (db.exists_table(Session_Info.table)) {
+      if (session_info_exists(db)) {
         db.execute_query_statementO[Store.Build_Info](
           Session_Info.table.select(sql = Session_Info.session_name.where_equal(name)),
           { res =>