deploy site from 2835aa9

leanprover-community · Feb 11, 2025 · 60abe37 · 60abe37
1 parent 8ce757c
commit 60abe37
Show file tree

Hide file tree

Showing 6 changed files with 510 additions and 496 deletions.
diff --git a/100.html b/100.html
diff --git a/1000.html b/1000.html
diff --git a/contribute/index.html b/contribute/index.html
@@ -167,7 +167,7 @@ <h2 id="making-a-pull-request-pr" class="markdown-heading">Making a Pull Request
 <p>Any other comments you want to keep out of the PR commit should go
 below the <code>---</code>.</p>
 <h2 id="lifecycle-of-a-pr" class="markdown-heading">Lifecycle of a PR <a class="hover-link" href="#lifecycle-of-a-pr">#</a></h2>
-<p>Many reviewers use the <a href="https://bit.ly/4eIDoOJ">review queue</a> to identify PRs that are ready for review.
+<p>Many reviewers use the <a href="../queue-redirect">review queue</a> 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 <code>#queue</code> on Zulip), and write reviews of PRs within their expertise.</p>
 <p>The review queue is controlled by GitHub &quot;labels&quot;.

diff --git a/mathlib_stats.html b/mathlib_stats.html
@@ -60,8 +60,8 @@ <h2>Counts</h2>
             <th>Contributors</th>
         </tr>
         <tr>
-            <td>96713</td>
-            <td>186881</td>
+            <td>96723</td>
+            <td>186899</td>
             <td>397</td>
         </tr>
     </table>