diff options
| author | Gereon Kremer <gkremer@stanford.edu> | 2021-05-04 19:06:35 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-04 17:06:35 +0000 |
| commit | 4f265b2c81c4cb858942f6e1e51ce8abdd01345b (patch) | |
| tree | 11059b0ebf4fd5ab9e0191af70809bd817e8a1bf /.github | |
| parent | 54845b5aba4e759c5a7db89226b9e824c7ef1d6c (diff) | |
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).
Diffstat (limited to '.github')
| -rw-r--r-- | .github/workflows/docs_update.yml | 20 |
1 files changed, 11 insertions, 9 deletions
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 |