eliminate somewhat obsolete augment_tables (see ff164add75cd), to support obsolete versions 10 and 9.x;
--- 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)))