From 638605d8fa645633b47b2ffd07c4309aeea72d6d Mon Sep 17 00:00:00 2001
From: Archmonger <16909269+Archmonger@users.noreply.github.com>
Date: Sat, 26 Aug 2023 14:15:09 -0700
Subject: [PATCH] Run `mike set-default` on release deployment

---
 .github/workflows/publish-release-docs.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/publish-release-docs.yml b/.github/workflows/publish-release-docs.yml
index a0c8861d..b58cb0ed 100644
--- a/.github/workflows/publish-release-docs.yml
+++ b/.github/workflows/publish-release-docs.yml
@@ -20,3 +20,4 @@ jobs:
                   git config user.name github-actions
                   git config user.email github-actions@github.com 
                   mike deploy --push --update-aliases ${{ github.event.release.name }} latest
+                  mike set-default --push latest