# HG changeset patch
# User wenzelm
# Date 1678281731 -3600
# Node ID 93f4b9164b9f9b84bb24b2be83bfbcd85541a361
# Parent  661d29a291ea496c58cf7043eb8c917f5562fafa
tuned;

diff -r 661d29a291ea -r 93f4b9164b9f src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Wed Mar 08 14:21:14 2023 +0100
+++ b/src/Pure/Admin/build_status.scala	Wed Mar 08 14:22:11 2023 +0100
@@ -24,7 +24,7 @@
     history: Int = 0,
     afp: Boolean = false,
     bulky: Boolean = false,
-    sql: String
+    sql: String = ""
   ) {
     def days(options: Options): Int = options.int("build_log_history") max history
 
@@ -37,15 +37,15 @@
       only_sessions: Set[String]
     ): PostgreSQL.Source = {
       Build_Log.Data.universal_table.select(columns, distinct = true, sql =
-        "WHERE " +
-          Build_Log.Data.pull_date(afp) + " > " + Build_Log.Data.recent_time(days(options)) +
-          " AND " +
-          Build_Log.Data.status.member(
-            List(
-              Build_Log.Session_Status.finished.toString,
-              Build_Log.Session_Status.failed.toString)) +
-          if_proper(only_sessions, " AND " + Build_Log.Data.session_name.member(only_sessions)) +
-          " AND " + SQL.enclose(sql))
+        SQL.where(
+          SQL.and(
+            Build_Log.Data.pull_date(afp).ident + " > " + Build_Log.Data.recent_time(days(options)),
+            Build_Log.Data.status.member(
+              List(
+                Build_Log.Session_Status.finished.toString,
+                Build_Log.Session_Status.failed.toString)),
+            if_proper(only_sessions, Build_Log.Data.session_name.member(only_sessions)),
+            if_proper(sql, SQL.enclose(sql)))))
     }
   }