diff options
Diffstat (limited to '.github/workflows/docs_upload.yml')
| -rw-r--r-- | .github/workflows/docs_upload.yml | 20 |
1 files changed, 13 insertions, 7 deletions
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 |