From 84b26096c24386d43012a55164a1fa6cebc937f4 Mon Sep 17 00:00:00 2001 From: timo Date: Thu, 9 Feb 2023 16:11:18 +0100 Subject: [PATCH] Cleanup workflow file There were some leftovers that were doing no harm, but I chose to remove them for clarity. --- .github/workflows/deploy-docs.yml | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/.github/workflows/deploy-docs.yml b/.github/workflows/deploy-docs.yml index 9f5a6e94f2..9b4c8b4048 100644 --- a/.github/workflows/deploy-docs.yml +++ b/.github/workflows/deploy-docs.yml @@ -1,6 +1,7 @@ name: Deploy Docs to GitHub Pages -on: # only on changes +on: + workflow_dispatch: push: branches: - '/v*' @@ -8,6 +9,9 @@ on: # only on changes paths: - 'docs/' +permissions: + contents: write + concurrency: group: docs cancel-in-progress: true @@ -42,10 +46,3 @@ jobs: with: github_token: ${{ secrets.GITHUB_TOKEN }} publish_dir: ./docs/build - # The following lines assign commit authorship to the official - # GH-Actions bot for deploys to `gh-pages` branch: - # https://github.com/actions/checkout/issues/13#issuecomment-724415212 - # The GH actions bot is used by default if you didn't specify the two fields. - # You can swap them out with your own user credentials. - user_name: github-actions[bot] - user_email: 41898282+github-actions[bot]@users.noreply.github.com