update #queue

leanprover-community · Sep 30, 2024 · ad1c63d · ad1c63d
1 parent bc2d66e
commit ad1c63d
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/.github/workflows/stale.yml b/.github/workflows/stale.yml
@@ -18,8 +18,8 @@ jobs:
           close-pr-message: 'Comment on the staled PRs while closed'
           days-before-stale: 60
           days-before-close: 120
-          # search string from the Zulip #queue link at https://bit.ly/3TJI3Yo
-          # "is:open is:pr -is:draft base:master sort:updated-asc status:success -label:blocked-by-other-PR -label:merge-conflict -label:awaiting-CI -label:WIP -label:awaiting-author -label:delegated -label:auto-merge-after-CI -label:ready-to-merge -label:please-adopt -label:help-wanted"
+          # search string from the Zulip #queue link at https://bit.ly/4eo6brN
+          # "is:open is:pr -is:draft base:master sort:updated-asc status:success -label:blocked-by-other-PR -label:merge-conflict -label:awaiting-CI -label:WIP -label:awaiting-author -label:delegated -label:auto-merge-after-CI -label:ready-to-merge -label:please-adopt -label:help-wanted -label:awaiting-zulip"
           # We want PRs _not_ on the queue, so we keep "is:pr -is:draft base:master" (is:open is added by the action by default) as a prefix for all queries and then negate the rest of the params in separate queries to simulate boolean OR (see https://github.com/actions/stale/pull/1145)
           # except for label:auto-merge-after-CI and label:ready-to-merge which presumably will be noticed before they go stale
-          only-matching-filter: '[ "is:pr -is:draft base:master -status:success", "is:pr -is:draft base:master label:blocked-by-other-PR", "is:pr -is:draft base:master label:merge-conflict", "is:pr -is:draft base:master label:awaiting-CI", "is:pr -is:draft base:master label:WIP", "is:pr -is:draft base:master label:awaiting-author", "is:pr -is:draft base:master label:delegated", "is:pr -is:draft base:master label:please-adopt", "is:pr -is:draft base:master label:help-wanted" ]'
+          only-matching-filter: '[ "is:pr -is:draft base:master -status:success", "is:pr -is:draft base:master label:blocked-by-other-PR", "is:pr -is:draft base:master label:merge-conflict", "is:pr -is:draft base:master label:awaiting-CI", "is:pr -is:draft base:master label:WIP", "is:pr -is:draft base:master label:awaiting-author", "is:pr -is:draft base:master label:delegated", "is:pr -is:draft base:master label:please-adopt", "is:pr -is:draft base:master label:help-wanted", "is:pr -is:draft base:master label:awaiting-zulip" ]'