GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-03 18:22:58 +03:00
Code Issues Projects Releases Wiki Activity

CI docs checkout merge sha not PR branch (may be on a fork).

Browse Source
This commit is contained in:
Kevin Quick 2023-06-21 16:27:51 -07:00
parent 8fefc47247
commit faa1a6c241
No known key found for this signature in database
GPG Key ID: E6D7733599CC0A21
1 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
.github/workflows/docs.yml vendored
View File

@ -112,15 +112,16 @@ jobs:
git -C ${REFREPO} fetch --all
for X in $(seq 0 $(( $(cat pulls.json | nix run nixpkgs#jq -- length) - 1))) ; do
prnum=$(cat pulls.json | nix run nixpkgs#jq -- .[${X}].number)
prbr=$(cat pulls.json | nix run nixpkgs#jq -- -r .[${X}].head.ref)
prref=$(cat pulls.json | nix run nixpkgs#jq -- -r .[${X}].merge_commit_sha)
tgt=${TGTBASE}/PR_${prnum}
echo "Checkout Pull Request ${prbr} into PR_${prnum}"
echo "Checkout Pull Request ${prnum} at ${prref} into PR_${prnum}"
mkdir $tgt
# n.b. the switch here is important to make sure the branch is
# present in the clone.
git -C ${REFREPO} switch --discard-changes ${prbr}
git -C ${REFREPO} fetch origin ${prref}
git -C ${REFREPO} checkout ${prref}
git clone ${REFREPO} ${tgt}
git -C ${tgt} switch --discard-changes ${prbr}
git -C ${tgt} checkout ${prref}
if [ ! -d ${tgt}/docs/RefMan ] ; then
echo "Removing ${tgt}: no RefMan docs in this version"
rm -rf ${tgt}