workflow/docs: Fix deployments

A couple fixes to make PRs and non-PRs work correctly:

* In a conditional expression, `true` or `false` are returned unless you
  terminate both sides in a ternary. That was causing 2 strings to be
  suffixed with `false` instead of an empty string.
* For a PR, we do actually want to cancel in progress runs since there's
  no danger of breaking an in progress deployment.
* For PRs, just use the same `github-pages-pr` name for the artifact.
  The important part is that it's not called `github-pages` where an in
  progress deployment could pick it up. Otherwise it can use the same
  name all the time.

diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 73bca6271584aefc1ef7c5f60cd76d4f496f4cba..9d9fe30ede539f8dca12f34ff61063bd46438e34 100644 (file)
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -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:
@@ -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