tuned;
authorwenzelm
Thu, 16 Mar 2023 15:58:34 +0100
changeset 77679 e92000492895
parent 77678 e7d8e990d378
child 77680 bc8e2fec9650
tuned;
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 " +