Have docs_upload properly upload tags. (#7352)

This PR improves our docs-ci mechanism to properly upload documentation for tags.

diff --git a/.github/workflows/docs_upload.yml b/.github/workflows/docs_upload.yml
index d9e81b05edb650bb63d8f1b5263d5108c56ebc34..8f51bab77496f4dbd4c3a1a1efcf25b144a517c9 100644 (file)
--- a/.github/workflows/docs_upload.yml
+++ b/.github/workflows/docs_upload.yml
@@ -55,7 +55,11 @@ jobs:
       - name: Setup Context
         run: |
           HASH=${{ github.event.workflow_run.head_commit.id }}
-          if [ "${{ github.event.workflow_run.event }}" == "push" ] ; then
+          ISTAG=${{ startsWith(github.ref, 'refs/tags/') }}
+          if [ "$ISTAG" ] ; then
+            NAME=${{ github.event.workflow_run.head_branch }}
+            echo "Identified tag $NAME"
+          elif [ "${{ github.event.workflow_run.event }}" == "push" ] ; then
             NAME=${{ github.event.workflow_run.head_branch }}
             echo "Identified branch $NAME"
           elif [ "${{ github.event.workflow_run.event }}" == "pull_request" ] ; then
@@ -66,6 +70,7 @@ jobs:
           fi
           echo "NAME=$NAME" >> $GITHUB_ENV
           echo "HASH=$HASH" >> $GITHUB_ENV
+          echo "ISTAG=$ISTAG" >> $GITHUB_ENV
 
       - name: Update docs
         continue-on-error: true
@@ -76,7 +81,10 @@ jobs:
             mv docs-new target/docs-$NAME-$HASH
             cd target/
 
-            if diff -r -x "*.zip" docs-master/ docs-$NAME-$HASH
+            (diff -r -x "*.zip" docs-master/ docs-$NAME-$HASH)
+            issame=$?
+
+            if [[ -n $ISTAG && $issame ]]
             then
               echo "Ignored run, documentation is the same as for current master"
             else