Skip to content

Commit

Permalink
[ admin ] Update ci-idris2-and-libs.yml
Browse files Browse the repository at this point in the history
Previous version of JamesIves/github-pages-deploy-action uses deprecated GH Actions functionality. It'll break eventually, better safe than sorry.
  • Loading branch information
CodingCellist authored Oct 23, 2023
1 parent 4097e6c commit 862d56c
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion .github/workflows/ci-idris2-and-libs.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down

0 comments on commit 862d56c

Please sign in to comment.