From 61a8f213190f70e311e9b4047e7f4e39df99d640 Mon Sep 17 00:00:00 2001 From: Catherine Date: Fri, 12 May 2023 13:19:30 +0000 Subject: [PATCH] CI: simplify publish-docs job. --- .github/workflows/main.yaml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/.github/workflows/main.yaml b/.github/workflows/main.yaml index c66a3a5..ab027bb 100644 --- a/.github/workflows/main.yaml +++ b/.github/workflows/main.yaml @@ -98,9 +98,6 @@ jobs: branch: main folder: docs/ target-folder: docs/amaranth/latest/ - - name: Extract release version - if: github.event_name == 'push' && startsWith(github.event.ref, 'refs/tags/v') - run: echo "VERSION=$(python setup.py --version)" >>$GITHUB_ENV - name: Publish release documentation if: github.event_name == 'push' && startsWith(github.event.ref, 'refs/tags/v') uses: JamesIves/github-pages-deploy-action@releases/v4 @@ -109,7 +106,7 @@ jobs: ssh-key: ${{ secrets.PAGES_DEPLOY_KEY }} branch: main folder: docs/ - target-folder: docs/amaranth/v${{ env.VERSION }}/ + target-folder: docs/amaranth/${{ github.ref_name }}/ publish-docs-dev: needs: document if: github.repository != 'amaranth-lang/amaranth'