From 862d56cce17e4f9c96e6229f5583db4c82dec620 Mon Sep 17 00:00:00 2001 From: CodingCellist Date: Mon, 23 Oct 2023 14:02:14 +0200 Subject: [PATCH] [ admin ] Update ci-idris2-and-libs.yml Previous version of JamesIves/github-pages-deploy-action uses deprecated GH Actions functionality. It'll break eventually, better safe than sorry. --- .github/workflows/ci-idris2-and-libs.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci-idris2-and-libs.yml b/.github/workflows/ci-idris2-and-libs.yml index 9cc21f6268..d2cc830682 100644 --- a/.github/workflows/ci-idris2-and-libs.yml +++ b/.github/workflows/ci-idris2-and-libs.yml @@ -762,7 +762,7 @@ jobs: cd - cp -r www/html/* .github/scripts/html/ - name: Deploy HTML - uses: JamesIves/github-pages-deploy-action@4.1.3 + uses: JamesIves/github-pages-deploy-action@4.4.3 if: ${{ success() && env.IDRIS2_DEPLOY }} with: