From fe337b8bf550a1e37bf744ef0870aab5c75ee7e4 Mon Sep 17 00:00:00 2001
From: Moshe Weitzman <weitzman@tejasa.com>
Date: Fri, 2 Aug 2024 08:43:36 -0400
Subject: [PATCH] Skip failing mike command

---
 .github/workflows/main.yml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index e3f5f70821..41c5575bfb 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -48,7 +48,8 @@ jobs:
       - name: Mike config
         run: |
           mike alias 13.x latest
-          mike set-default latest
+      # No longer needed.
+      # mike set-default latest
       - name: Mike deploy
         run: mike deploy --push ${GITHUB_REF_NAME}
       # Build Doctum to gh-pages/api in the gh-pages branch.