Fix GitHub Codespaces links to release tag after build with mike

Author: ewels

.github/workflows/release-docs.yml

@@ -10,13 +10,25 @@ jobs:
   deploy:
     runs-on: ubuntu-latest
     steps:
+
       - uses: actions/checkout@v4
         with:
           fetch-depth: 0
+
       - uses: actions/setup-python@v5
         with:
           python-version: 3.10.6
+
       - name: Install Dependencies
         run: pip install -r requirements.txt
+
       - name: Build Docs Website
-        run: mike deploy --push --alias-type copy --update-aliases ${{ github.event.release.tag_name }} latest
+        run: mike deploy --alias-type copy --update-aliases ${{ github.event.release.tag_name }} latest
+
+      - name: Pin GitHub Codespaces version
+        run: |
+          git checkout gh-pages
+          find ${{ github.event.release.tag_name }} -type f -exec sed -i 's|ref=master|ref=${{ github.event.release.tag_name }}|g' {} +
+          find latest -type f -exec sed -i 's|ref=master|ref=${{ github.event.release.tag_name }}|g' {} +
+          git commit -am "Pin GitHub Codespaces link versions"
+          git push