Use proper commit hash for PRs (#6485)

For PRs, the automatically generated documentation is stored under the current master commit hash instead of the hash of the latest commit on the PR. This PR fixes this issue by exporting the commit hash (much like the name of the PR or branch).

diff --git a/.github/workflows/docs_update.yml b/.github/workflows/docs_update.yml
index 9c733728ff4432c4a2ed86664f9cbd6e8984a3cd..e9244cec3e3adef4a172747144f1fc7a670f6b89 100644 (file)
--- a/.github/workflows/docs_update.yml
+++ b/.github/workflows/docs_update.yml
@@ -57,21 +57,23 @@ jobs:
           git config --global user.name "DocBot"
           if [ "${{ github.event_name }}" == "push" ] ; then
             NAME=$(echo "${GITHUB_REF}" | sed "s,refs/heads/,,")
+            HASH=${{ github.sha }}
             echo "Identified branch $NAME"
           elif [ "${{ github.event_name }}" == "pull_request_target" ] ; then
             NAME="${{ github.event.number }}"
-            PRHASH="${{ github.event.pull_request.head.sha }}"
-            echo "Identified PR #$NAME (from $PRHASH)"
+            HASH="${{ github.event.pull_request.head.sha }}"
+            echo "Identified PR #$NAME (from $HASH)"
             NAME="pr$NAME"
             # be careful here, see explanation above!
             git remote add pr "${{ github.event.pull_request.head.repo.clone_url}}"
             git fetch pr "${{ github.event.pull_request.head.ref}}:pr"
-            git checkout "${PRHASH}" -- \
-              `git ls-tree "${PRHASH}" --name-only -r docs/ | grep -E ".*\.(rst|bib)"` \
-              `git ls-tree "${PRHASH}" --name-only -r src/api/ | grep -E ".*\.(h|cpp|java|py)"` \
-              `git ls-tree "${PRHASH}" --name-only -r examples/ | grep -E ".*\.(h|cpp|java|py|smt2)"`
+            git checkout "${HASH}" -- \
+              `git ls-tree "${HASH}" --name-only -r docs/ | grep -E ".*\.(rst|bib)"` \
+              `git ls-tree "${HASH}" --name-only -r src/api/ | grep -E ".*\.(h|cpp|java|py)"` \
+              `git ls-tree "${HASH}" --name-only -r examples/ | grep -E ".*\.(h|cpp|java|py|smt2)"`
           fi
           echo "NAME=$NAME" >> $GITHUB_ENV
+          echo "HASH=$HASH" >> $GITHUB_ENV
 
       - name: Configure
         run: ./configure.sh production --docs --all-bindings --auto-download
@@ -94,11 +96,11 @@ jobs:
         run: |
           git clone git@github.com:cvc5/docs-ci.git target/
           if [ -n "$NAME" ]; then
-            rsync -a --delete build/docs/sphinx-gh/ target/docs-$NAME-${{ github.sha }}
+            rsync -a --delete build/docs/sphinx-gh/ target/docs-$NAME-$HASH
             cd target/
             rm -f docs-$NAME
-            ln -s docs-$NAME-${{ github.sha }} docs-$NAME
-            git add docs-$NAME docs-$NAME-${{ github.sha }}
+            ln -s docs-$NAME-$HASH docs-$NAME
+            git add docs-$NAME docs-$NAME-$HASH
 
             python3 genindex.py
             git add README.md