# HG changeset patch
# User wenzelm
# Date 1678978714 -3600
# Node ID e92000492895ad13d3222bb6cf5a8cc60e5c342b
# Parent  e7d8e990d37856b3e111e933e1b5116bbc20a84e
tuned;

diff -r e7d8e990d378 -r e92000492895 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Thu Mar 16 15:55:49 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Thu Mar 16 15:58:34 2023 +0100
@@ -631,7 +631,7 @@
 
   object Data {
     def build_log_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table =
-      SQL.Table("isabelle_build_log_" + name, columns, body)
+      SQL.Table("isabelle_build_log" + if_proper(name, "_" + name), columns, body)
 
 
     /* main content */
@@ -797,7 +797,7 @@
           b_table.query_named + SQL.join_inner + sessions_table +
           " ON " + log_name(b_table) + " = " + log_name(sessions_table))
 
-      SQL.Table("isabelle_build_log", c_columns ::: List(ml_statistics),
+      build_log_table("", c_columns ::: List(ml_statistics),
         {
           SQL.select(c_columns.map(_.apply(c_table)) ::: List(ml_statistics)) +
           c_table.query_named + SQL.join_outer + ml_statistics_table + " ON " +