From: Gereon Kremer <nafur42@gmail.com>
Date: Wed, 20 Oct 2021 23:45:48 +0000 (-0700)
Subject: Fix docs upload (again) (#7435)
X-Git-Tag: cvc5-1.0.0~1026
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f730e8a89b329d029ccae8aa2637bb19a7360f0c;p=cvc5.git

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 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