From d39147aa10c2520415e2d38ec3a4a69cceae1dbe Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Thu, 18 May 2023 16:59:21 +0000 Subject: [PATCH 1/3] Bump Andrew-Chen-Wang/github-wiki-action from 3 to 4 Bumps [Andrew-Chen-Wang/github-wiki-action](https://github.com/Andrew-Chen-Wang/github-wiki-action) from 3 to 4. - [Release notes](https://github.com/Andrew-Chen-Wang/github-wiki-action/releases) - [Commits](https://github.com/Andrew-Chen-Wang/github-wiki-action/compare/v3...v4) --- updated-dependencies: - dependency-name: Andrew-Chen-Wang/github-wiki-action dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 45ff5bc58..3f4bd3cf3 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -57,7 +57,7 @@ jobs: # This step would err if the forked repo does not already have wiki pages. # As a workaround, it is disabled for all forked repos. if: ${{ github.repository_owner == 'HoTT' && github.ref == 'refs/heads/master' }} - uses: Andrew-Chen-Wang/github-wiki-action@v3 + uses: Andrew-Chen-Wang/github-wiki-action@v4 env: WIKI_DIR: "./_wiki_dir/" GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} From e1da0e40cf176b21d9fb1ee18b165b9b1c0d0f1b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 May 2023 06:27:20 -0700 Subject: [PATCH 2/3] Adjust action syntax for new action version --- .github/workflows/ci.yml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3f4bd3cf3..cdbee7753 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -58,8 +58,5 @@ jobs: # As a workaround, it is disabled for all forked repos. if: ${{ github.repository_owner == 'HoTT' && github.ref == 'refs/heads/master' }} uses: Andrew-Chen-Wang/github-wiki-action@v4 - env: - WIKI_DIR: "./_wiki_dir/" - GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} - GH_NAME: "github-actions" - GH_MAIL: "github-actions@github.com" + with: + path: "./_wiki_dir/" From 7ad08505c12380e26cadf9b0794a642e55b5b556 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 May 2023 06:29:05 -0700 Subject: [PATCH 3/3] [ci] remove useless slashes --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index cdbee7753..79c2376b6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -59,4 +59,4 @@ jobs: if: ${{ github.repository_owner == 'HoTT' && github.ref == 'refs/heads/master' }} uses: Andrew-Chen-Wang/github-wiki-action@v4 with: - path: "./_wiki_dir/" + path: _wiki_dir