5 echo "Removing the current docs for master"
6 rm -rf out/master/ || exit 0
8 echo "Making the docs for master"
10 cp util/gh-pages/index.html out/master
11 cp util/gh-pages/lints.json out/master
13 if [[ -n $TAG_NAME ]]; then
14 echo "Save the doc for the current tag ($TAG_NAME) and point stable/ to it"
15 cp -Tr out/master "out/$TAG_NAME"
16 ln -sf "$TAG_NAME" out/stable
19 if [[ $BETA = "true" ]]; then
20 echo "Update documentation for the beta release"
21 cp -r out/master/* out/beta
24 # Generate version index that is shown as root index page
25 cp util/gh-pages/versions.html out/index.html
27 echo "Making the versions.json file"
28 python3 ./util/versions.py out
30 # Now let's go have some fun with the cloned repo
32 git config user.name "GHA CI"
33 git config user.email "gha@ci.invalid"
35 if [[ -n $TAG_NAME ]]; then
36 # track files, so that the following check works
37 git add --intent-to-add "$TAG_NAME"
38 if git diff --exit-code --quiet -- $TAG_NAME/; then
39 echo "No changes to the output on this push; exiting."
46 # Update versions file
48 git commit -m "Add documentation for ${TAG_NAME} release: ${SHA}"
49 elif [[ $BETA = "true" ]]; then
50 if git diff --exit-code --quiet -- beta/; then
51 echo "No changes to the output on this push; exiting."
55 git commit -m "Automatic deploy to GitHub Pages (beta): ${SHA}"
57 if git diff --exit-code --quiet; then
58 echo "No changes to the output on this push; exiting."
62 git commit -m "Automatic deploy to GitHub Pages: ${SHA}"
65 git push "$SSH_REPO" "$TARGET_BRANCH"