Skip to content

ci: Only commit and push if there are changes #8

ci: Only commit and push if there are changes

ci: Only commit and push if there are changes #8

Workflow file for this run

on: [push, pull_request]
name: Build and Deploy
jobs:
build:
runs-on: ubuntu-latest
steps:
- name: Checkout code
uses: actions/checkout@v4
- name: Install requirements
run: |
pip install -r beginners/requirements.txt
- name: Build GitHub pages
run: |
cd beginners
make github
- name: Deploy tutorial on the cvc5 website
if: (github.repository == 'cvc5/tutorials') && (github.ref == 'refs/heads/main')
run: |
git config --global user.email "[email protected]"
git config --global user.name "cvc5-bot"
git clone https://github.com/cvc5/cvc5.github.io.git website
rm -r website/tutorials/beginners
cp -r beginners/_build/html website/tutorials/beginners
cd website/
git add tutorials/beginners
# 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