# HG changeset patch
# User wenzelm
# Date 1688837577 -7200
# Node ID 30d035a83dbeead4a4c2d8154e34945df45a9fd2
# Parent  c0dc000d2a40c1984649b94ad671fd0be14bf4d0
eliminate somewhat obsolete augment_tables (see ff164add75cd), to support obsolete versions 10 and 9.x;

diff -r c0dc000d2a40 -r 30d035a83dbe src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Sat Jul 08 19:28:26 2023 +0200
+++ b/src/Pure/Thy/store.scala	Sat Jul 08 19:32:57 2023 +0200
@@ -103,10 +103,6 @@
       val build_columns = List(sources, input_heaps, output_heap, return_code, uuid)
 
       val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
-
-      val augment_table: PostgreSQL.Source =
-        "ALTER TABLE IF EXISTS " + table.ident +
-        " ADD COLUMN IF NOT EXISTS " + uuid.decl(SQL.sql_type_postgresql)
     }
 
     object Sources {
@@ -429,7 +425,6 @@
       db.execute_statement(
         Store.Data.Session_Info.table.delete(
           sql = Store.Data.Session_Info.session_name.where_equal(name)))
-      if (db.is_postgresql) db.execute_statement(Store.Data.Session_Info.augment_table)
 
       db.execute_statement(Store.Data.Sources.table.delete(
         sql = Store.Data.Sources.where_equal(name)))