# HG changeset patch
# User wenzelm
# Date 1699471889 -3600
# Node ID 2fee5fba3116771dc0930e4e1f89e9e57369f3ed
# Parent  e495f910dd948a32d5558c8dafa44a6b7840886f
proper default for disjunction (amending 9f7a94117666);

diff -r e495f910dd94 -r 2fee5fba3116 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Wed Nov 08 19:04:44 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Wed Nov 08 20:31:29 2023 +0100
@@ -720,8 +720,8 @@
 
     /* recent entries */
 
-    def recent(c: SQL.Column, days: Int): PostgreSQL.Source =
-      if (days <= 0) ""
+    def recent(c: SQL.Column, days: Int, default: PostgreSQL.Source = ""): PostgreSQL.Source =
+      if (days <= 0) default
       else c.ident + " > now() - INTERVAL '" + days + " days'"
 
     def recent_pull_date_table(
@@ -739,7 +739,7 @@
       SQL.Table("recent_pull_date", table.columns,
         table.select(table.columns, sql =
           SQL.where_or(
-            recent(pull_date(afp)(table), days),
+            recent(pull_date(afp)(table), days, default = SQL.TRUE),
             SQL.and(eq_rev, eq_rev2))))
     }