# HG changeset patch
# User wenzelm
# Date 1677526748 -3600
# Node ID ca3fe041f8672d98bc02bb5f3d5fb8396abb0d5e
# Parent  be8e14c7da800da0618b48fd115bc274aeee3f4a
tuned;

diff -r be8e14c7da80 -r ca3fe041f867 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon Feb 27 20:30:40 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Mon Feb 27 20:39:08 2023 +0100
@@ -1062,13 +1062,6 @@
       val table1 = Data.sessions_table
       val table2 = Data.ml_statistics_table
 
-      val where =
-        SQL.where(
-          SQL.and(
-            Data.log_name(table1).equal(log_name),
-            Data.session_name(table1).ident + " <> ''",
-            if_proper(session_names, Data.session_name(table1).member(session_names))))
-
       val columns1 = table1.columns.tail.map(_.apply(table1))
       val (columns, from) =
         if (ml_statistics) {
@@ -1082,6 +1075,13 @@
         }
         else (columns1, table1.ident)
 
+      val where =
+        SQL.where(
+          SQL.and(
+            Data.log_name(table1).equal(log_name),
+            Data.session_name(table1).ident + " <> ''",
+            if_proper(session_names, Data.session_name(table1).member(session_names))))
+
       val sessions =
         db.using_statement(SQL.select(columns, sql = from + where)) { stmt =>
           stmt.execute_query().iterator({ res =>