From: Gereon Kremer <gkremer@stanford.edu>
Date: Tue, 4 May 2021 17:06:35 +0000 (+0200)
Subject: Use proper commit hash for PRs (#6485)
X-Git-Tag: cvc5-1.0.0~1796
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4f265b2c81c4cb858942f6e1e51ce8abdd01345b;p=cvc5.git

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 9c733728f..e9244cec3 100644
--- 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