diff options
Diffstat (limited to '.github')
| -rw-r--r-- | .github/workflows/docs_cleanup.yml | 10 | ||||
| -rw-r--r-- | .github/workflows/docs_upload.yml | 20 |
2 files changed, 21 insertions, 9 deletions
diff --git a/.github/workflows/docs_cleanup.yml b/.github/workflows/docs_cleanup.yml index 67b5f6b4a..f56a0f595 100644 --- a/.github/workflows/docs_cleanup.yml +++ b/.github/workflows/docs_cleanup.yml @@ -4,8 +4,9 @@ on: - cron: '0 1 * * SUN' jobs: - build: + docs-cleanup: runs-on: ubuntu-latest + if: github.repository == 'cvc5/cvc5' steps: - name: Install Packages run: | @@ -58,6 +59,11 @@ jobs: python3 genindex.py git add README.md - git commit -m "Update README.md" + if git diff --cached --exit-code + then + echo "Nothing changed" + else + git commit -m "Update README.md" + fi git push -f diff --git a/.github/workflows/docs_upload.yml b/.github/workflows/docs_upload.yml index 356337de6..7346371e3 100644 --- a/.github/workflows/docs_upload.yml +++ b/.github/workflows/docs_upload.yml @@ -75,15 +75,21 @@ jobs: if [ -n "$NAME" ]; then mv docs-new target/docs-$NAME-$HASH cd target/ - rm -f docs-$NAME - ln -s docs-$NAME-$HASH docs-$NAME - git add docs-$NAME docs-$NAME-$HASH - python3 genindex.py - git add README.md - git commit -m "Update docs for $NAME" + if diff -r target/docs-master/ target/docs-$NAME-$HASH + then + echo "Ignored run, documentation is the same as for current master" + else + rm -f docs-$NAME + ln -s docs-$NAME-$HASH docs-$NAME + git add docs-$NAME docs-$NAME-$HASH - git push + python3 genindex.py + git add README.md + git commit -m "Update docs for $NAME" + + git push + fi else echo "Ignored run" fi |