From 4e6a2e16ed2d816c074e78db0f4a8d013b90ffb8 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Mon, 16 Sep 2024 13:50:07 -0500 Subject: [PATCH] ci: Only commit if there are changes --- .github/workflows/main.yml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index a792d98..78bece1 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -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