Merge pull request #3305 from dbnicholson/pages-fixes

workflow/docs: Fix deployments
This commit is contained in:
Colin Walters 2024-09-15 16:39:38 -04:00 committed by GitHub
commit 2945165ffe
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194

View File

@ -15,10 +15,11 @@ on:
# want to allow these production deployments to complete. # want to allow these production deployments to complete.
# #
# Since pull requests use a unique artifact name and won't be deployed, they # Since pull requests use a unique artifact name and won't be deployed, they
# shouldn't be limited. Use a unique group name in that case. # shouldn't be limited. Use a unique group name in that case and let in
# progress runs be cancelled.
concurrency: concurrency:
group: "pages${{ github.event_name == 'pull_request' && format('-pr{0}', github.event.number) }}" group: "pages${{ github.event_name == 'pull_request' && format('-pr{0}', github.event.number) || '' }}"
cancel-in-progress: false cancel-in-progress: ${{ github.event_name == 'pull_request' }}
jobs: jobs:
build: build:
@ -57,9 +58,9 @@ jobs:
with: with:
path: docs/_site path: docs/_site
# The default name is github-pages to match actions/deploy-pages. For # The default name is github-pages to match actions/deploy-pages. For
# PRs use a unique name so results can be inspected without # PRs use a different name so results can be inspected without real
# interfering with real deployments. # deployments accidentally getting the wrong artifact.
name: "github-pages${{ github.event_name == 'pull_request' && format('-pr{0}', github.event.number) }}" name: "github-pages${{ github.event_name == 'pull_request' && '-pr' || '' }}"
deploy: deploy:
name: Deploy documentation name: Deploy documentation