From 7908a99c0ae2477b1c67211d17aeb09cf0176f28 Mon Sep 17 00:00:00 2001 From: Davide Bettio Date: Mon, 14 Oct 2024 13:30:35 +0200 Subject: [PATCH] CI: publish-docs: do not make it conditional Always run it, and just skip single commit and push commands. Signed-off-by: Davide Bettio --- .github/workflows/publish-docs.yaml | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/.github/workflows/publish-docs.yaml b/.github/workflows/publish-docs.yaml index 0d282d03b..bba3fe001 100644 --- a/.github/workflows/publish-docs.yaml +++ b/.github/workflows/publish-docs.yaml @@ -124,13 +124,11 @@ jobs: git checkout Production git config --local user.email "atomvm-doc-bot@users.noreply.github.com" git config --local user.name "AtomVM Doc Bot" - if [ -n "$(git status --porcelain=v1)" ]; then - git add . - git commit -m "Update Documentation" - echo "PUBLISH=true" >> "$GITHUB_OUTPUT" - fi + ls -la doc/ + git add . + git diff --exit-code || git commit -m "Update Documentation" - name: Push changes - if: github.repository == 'atomvm/AtomVM' && steps.commit_files.outputs.PUBLISH == 'true' + if: github.repository == 'atomvm/AtomVM' working-directory: /home/runner/work/AtomVM/AtomVM/www run: | eval `ssh-agent -t 60 -s` @@ -139,4 +137,4 @@ jobs: ssh-keyscan github.com >> ~/.ssh/known_hosts git remote add push_dest "git@github.com:atomvm/atomvm_www.git" git fetch push_dest - git push --set-upstream push_dest Production + git diff --exit-code origin/Production || git push --set-upstream push_dest Production