Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

workflow/docs: Fix deployments #3305

Merged
merged 1 commit into from
Sep 15, 2024
Merged

workflow/docs: Fix deployments #3305

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 7 additions & 6 deletions .github/workflows/docs.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,11 @@ on:
# want to allow these production deployments to complete.
#
# 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:
group: "pages${{ github.event_name == 'pull_request' && format('-pr{0}', github.event.number) }}"
cancel-in-progress: false
group: "pages${{ github.event_name == 'pull_request' && format('-pr{0}', github.event.number) || '' }}"
cancel-in-progress: ${{ github.event_name == 'pull_request' }}

jobs:
build:
Expand Down Expand Up @@ -57,9 +58,9 @@ jobs:
with:
path: docs/_site
# The default name is github-pages to match actions/deploy-pages. For
# PRs use a unique name so results can be inspected without
# interfering with real deployments.
name: "github-pages${{ github.event_name == 'pull_request' && format('-pr{0}', github.event.number) }}"
# PRs use a different name so results can be inspected without real
# deployments accidentally getting the wrong artifact.
name: "github-pages${{ github.event_name == 'pull_request' && '-pr' || '' }}"

deploy:
name: Deploy documentation
Expand Down
Loading