add self-hosted #queue redirect (#590)

Unfortunately bit.ly is going to start forcing free users to click through a page with ads. As an alternative, we'll host a simple redirect page here instead. I'll update the `#queue` linkifier on Zulip to point to https://leanprover-community.github.io/queue-redirect after this is merged.
leanprover-community · Feb 11, 2025 · 2835aa9 · 2835aa9
1 parent ac1f141
commit 2835aa9
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 3 deletions.
diff --git a/templates/contribute/index.md b/templates/contribute/index.md
@@ -109,15 +109,15 @@ below the `---`.
 
 ## Lifecycle of a PR
 
-Many reviewers use the [review queue](https://bit.ly/4eIDoOJ) to identify PRs that are ready for review.
+Many reviewers use the [review queue](../queue-redirect) to identify PRs that are ready for review.
 The instructions below will ensure that your PR appears on that queue; if it doesn't appear there it may not receive much attention.
 Everyone is also invited to regularly look at the queue (it is linkified as `#queue` on Zulip), and write reviews of PRs within their expertise.
 
-The review queue is controlled by GitHub "labels". 
+The review queue is controlled by GitHub "labels".
 On the main page for a PR, on the right-hand side,
 there should be a sidebar with panels "reviewers", "assignees", "labels", etc.
 Click on the "labels" header to add or remove labels from the current project.
-(Labels can only be edited by "GitHub collaborators", which is approximately the same as "people who have asked for write access".) 
+(Labels can only be edited by "GitHub collaborators", which is approximately the same as "people who have asked for write access".)
 
 If your PR builds (has a green checkmark), someone will probably "review" it within a few days (depending on the size of the PR; smaller PRs will get quicker responses). The reviewer will probably leave comments and add the label **"awaiting-author"**. You should address each comment, clicking the "resolve conversation" button once the problem is resolved. Ideally each problem is resolved with a new commit, but there is no hard rule here. Once all requested changes are implemented, you should remove the **"awaiting-author"** label to start the process over again.
 

diff --git a/templates/queue-redirect.html b/templates/queue-redirect.html
@@ -0,0 +1,14 @@
+<!DOCTYPE HTML>
+<html lang="en-US">
+    <head>
+        <meta charset="UTF-8">
+        <meta http-equiv="refresh" content="0; url=https://github.com/leanprover-community/mathlib4/pulls?q=is:open+is:pr+-is:draft+base:master+sort:updated-asc+status:success+-label:blocked-by-other-PR+-label:blocked-by-batt-PR+-label:blocked-by-core-PR+-label:blocked-by-qq-PR+-label:merge-conflict+-label:awaiting-author+-label:awaiting-CI+-label:awaiting-zulip+-label:WIP+-label:delegated+-label:auto-merge-after-CI+-label:ready-to-merge+-label:please-adopt+-label:help-wanted">
+        <script type="text/javascript">
+            window.location.href = "https://github.com/leanprover-community/mathlib4/pulls?q=is:open+is:pr+-is:draft+base:master+sort:updated-asc+status:success+-label:blocked-by-other-PR+-label:blocked-by-batt-PR+-label:blocked-by-core-PR+-label:blocked-by-qq-PR+-label:merge-conflict+-label:awaiting-author+-label:awaiting-CI+-label:awaiting-zulip+-label:WIP+-label:delegated+-label:auto-merge-after-CI+-label:ready-to-merge+-label:please-adopt+-label:help-wanted"
+        </script>
+        <title>Mathlib #queue</title>
+    </head>
+    <body>
+        If you are not redirected automatically, follow this <a href='https://github.com/leanprover-community/mathlib4/pulls?q=is:open+is:pr+-is:draft+base:master+sort:updated-asc+status:success+-label:blocked-by-other-PR+-label:blocked-by-batt-PR+-label:blocked-by-core-PR+-label:blocked-by-qq-PR+-label:merge-conflict+-label:awaiting-author+-label:awaiting-CI+-label:awaiting-zulip+-label:WIP+-label:delegated+-label:auto-merge-after-CI+-label:ready-to-merge+-label:please-adopt+-label:help-wanted'>link to the mathlib #queue</a>.
+    </body>
+</html>