Fix docs upload (again) (#7435)

This is a follow-up to #7420. This time, I tested the modified code with every combination of values...

diff --git a/.github/workflows/docs_upload.yml b/.github/workflows/docs_upload.yml
index f6ee6a0d315fac2f66981b2fb39fc28d22979301..7bdd186a1654277d0e8e25e83f58ed65ba9b4e00 100644 (file)
--- 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