diff options
Diffstat (limited to '.github/workflows/docs_upload.yml')
| -rw-r--r-- | .github/workflows/docs_upload.yml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/.github/workflows/docs_upload.yml b/.github/workflows/docs_upload.yml index f6ee6a0d3..7bdd186a1 100644 --- a/.github/workflows/docs_upload.yml +++ b/.github/workflows/docs_upload.yml @@ -56,7 +56,7 @@ jobs: run: | HASH=${{ github.event.workflow_run.head_commit.id }} ISTAG=${{ startsWith(github.ref, 'refs/tags/') }} - if [ "$ISTAG" ] ; then + if [ "$ISTAG" = true ] ; then NAME=${{ github.event.workflow_run.head_branch }} echo "Identified tag $NAME" elif [ "${{ github.event.workflow_run.event }}" == "push" ] ; then @@ -81,9 +81,9 @@ jobs: mv docs-new target/docs-$NAME-$HASH cd target/ - issame=$(diff -r -x "*.zip" docs-master/ docs-$NAME-$HASH; echo $?; exit 0) + isdiff=$(diff -r -x "*.zip" docs-master/ docs-$NAME-$HASH >&2; echo $?; exit 0) - if [[ -n $ISTAG && $issame ]] + if [[ ("$ISTAG" != true) && ($isdiff = 0) ]] then echo "Ignored run, documentation is the same as for current master" else |