mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-30 03:46:02 +03:00
Update CI docs git clone/checkout process.
This commit is contained in:
parent
8ef8ef4a82
commit
8fefc47247
52
.github/workflows/docs.yml
vendored
52
.github/workflows/docs.yml
vendored
@ -77,8 +77,6 @@ jobs:
|
|||||||
name: github-pages
|
name: github-pages
|
||||||
url: ${{ steps.deployment.outputs.page_url }}
|
url: ${{ steps.deployment.outputs.page_url }}
|
||||||
env:
|
env:
|
||||||
# GH_TOKEN is used to enable the `gh repo clone` below.
|
|
||||||
GH_TOKEN: ${{ github.token }}
|
|
||||||
# TGTBASE is used below as the working location to checkout and generate
|
# TGTBASE is used below as the working location to checkout and generate
|
||||||
# documentation. Can be changed for convenience.
|
# documentation. Can be changed for convenience.
|
||||||
TGTBASE: docs/ci_build_out
|
TGTBASE: docs/ci_build_out
|
||||||
@ -107,44 +105,40 @@ jobs:
|
|||||||
run: |
|
run: |
|
||||||
rm -rf ${TGTBASE}
|
rm -rf ${TGTBASE}
|
||||||
mkdir ${TGTBASE}
|
mkdir ${TGTBASE}
|
||||||
gh repo clone ${{ github.repositoryURL }} ${REFREPO}
|
# n.b. do not use github.repositoryURL for checkout: it is
|
||||||
git -C ${REFREPO} switch --discard-changes master
|
# git:/github.com/owner/repo but that will fail in the context of
|
||||||
echo local branches
|
# github workflows; use an https reference instead:
|
||||||
git -C ${REFREPO} branch -l
|
git -c protocol.version=2 clone ${{ github.server_url }}/${{ github.repository }} ${REFREPO}
|
||||||
echo remote branches
|
git -C ${REFREPO} fetch --all
|
||||||
git -C ${REFREPO} branch -l -r
|
|
||||||
for X in $(seq 0 $(( $(cat pulls.json | nix run nixpkgs#jq -- length) - 1))) ; do
|
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)
|
prnum=$(cat pulls.json | nix run nixpkgs#jq -- .[${X}].number)
|
||||||
prbr=$(cat pulls.json | nix run nixpkgs#jq -- -r .[${X}].head.ref)
|
prbr=$(cat pulls.json | nix run nixpkgs#jq -- -r .[${X}].head.ref)
|
||||||
tgt=${TGTBASE}/PR_${prnum}
|
tgt=${TGTBASE}/PR_${prnum}
|
||||||
echo "Checkout Pull Request ${prbr} into PR_${prnum}"
|
echo "Checkout Pull Request ${prbr} into PR_${prnum}"
|
||||||
(set -x
|
mkdir $tgt
|
||||||
mkdir $tgt
|
# n.b. the switch here is important to make sure the branch is
|
||||||
git clone -b ${prbr} --single-branch ${REFREPO} ${tgt}
|
# present in the clone.
|
||||||
ls -a ${tgt}
|
git -C ${REFREPO} switch --discard-changes ${prbr}
|
||||||
echo lbr
|
|
||||||
git -C ${tgt} branch -l
|
|
||||||
echo rbr
|
|
||||||
git -C ${tgt} branch -l -r
|
|
||||||
echo switch
|
|
||||||
git -C ${tgt} switch --discard-changes ${prbr}
|
|
||||||
if [ ! -d ${tgt}/docs/RefMan ] ; then
|
|
||||||
echo "Removing ${tgt}: no RefMan docs in this version"
|
|
||||||
rm -rf ${tgt}
|
|
||||||
fi
|
|
||||||
)
|
|
||||||
done
|
|
||||||
for X in $(seq 0 $(( $(cat tags.json | nix run nixpkgs#jq -- length) - 1))) ; do
|
|
||||||
tagname=$(cat tags.json | nix run nixpkgs#jq -- -r .[${X}].name)
|
|
||||||
tgt=${TGTBASE}/${tagname}
|
|
||||||
echo "Checkout Release Tag ${tagname} into ${tagname}"
|
|
||||||
git clone ${REFREPO} ${tgt}
|
git clone ${REFREPO} ${tgt}
|
||||||
git -C ${tgt} checkout --detach ${tagname}
|
git -C ${tgt} switch --discard-changes ${prbr}
|
||||||
if [ ! -d ${tgt}/docs/RefMan ] ; then
|
if [ ! -d ${tgt}/docs/RefMan ] ; then
|
||||||
echo "Removing ${tgt}: no RefMan docs in this version"
|
echo "Removing ${tgt}: no RefMan docs in this version"
|
||||||
rm -rf ${tgt}
|
rm -rf ${tgt}
|
||||||
fi
|
fi
|
||||||
done
|
done
|
||||||
|
for X in $(seq 0 $(( $(cat tags.json | nix run nixpkgs#jq -- length) - 1))) ; do
|
||||||
|
tagname=$(cat tags.json | nix run nixpkgs#jq -- -r .[${X}].name)
|
||||||
|
tgt=${TGTBASE}/${tagname}
|
||||||
|
echo "Checkout Release Tag ${tagname} into ${tagname}"
|
||||||
|
git -C ${REFREPO} checkout ${tagname}
|
||||||
|
git clone ${REFREPO} ${tgt}
|
||||||
|
git -C ${tgt} checkout ${tagname}
|
||||||
|
if [ ! -d ${tgt}/docs/RefMan ] ; then
|
||||||
|
echo "Removing ${tgt}: no RefMan docs in this version"
|
||||||
|
rm -rf ${tgt}
|
||||||
|
fi
|
||||||
|
done
|
||||||
|
git -C ${REFREPO} switch --discard-changes master
|
||||||
- name: sphinx version config for each doc directory
|
- name: sphinx version config for each doc directory
|
||||||
shell: bash
|
shell: bash
|
||||||
run: |
|
run: |
|
||||||
|
Loading…
Reference in New Issue
Block a user