Skip to content

Commit

Permalink
Merge pull request #5 from daniel-larraz/check-changes
Browse files Browse the repository at this point in the history
ci: Only commit and push if there are changes
  • Loading branch information
daniel-larraz authored Sep 16, 2024
2 parents 9e9cc6a + 4e6a2e1 commit 0581b7b
Showing 1 changed file with 9 additions and 2 deletions.
11 changes: 9 additions & 2 deletions .github/workflows/main.yml
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,13 @@ jobs:
rm -r website/tutorials/beginners
cp -r beginners/_build/html website/tutorials/beginners
cd website/
git add tutorials/beginners
git commit -m "Deploy tutorials from source repo"
git push https://$GITHUB_ACTOR:${{ secrets.CVC5_WEBSITE_TOKEN }}@github.com/cvc5/cvc5.github.io.git main
# Check if there is anything to commit
if ! git diff --staged --quiet; then
git commit -m "Deploy tutorials from source repo"
git push https://$GITHUB_ACTOR:${{ secrets.CVC5_WEBSITE_TOKEN }}@github.com/cvc5/cvc5.github.io.git main
else
echo "No changes to commit"
fi

0 comments on commit 0581b7b

Please sign in to comment.