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 python ./util/export.py out/master/lints.json
13 if [[ -n $TAG_NAME ]]; then
14 echo "Save the doc for the current tag ($TAG_NAME) and point current/ to it"
15 cp -r out/master "out/$TAG_NAME"
17 ln -s "$TAG_NAME" out/current
20 # Generate version index that is shown as root index page
21 cp util/gh-pages/versions.html out/index.html
23 echo "Making the versions.json file"
24 python ./util/versions.py out
27 # Now let's go have some fun with the cloned repo
28 git config user.name "GHA CI"
29 git config user.email "gha@ci.invalid"
31 if git diff --exit-code --quiet; then
32 echo "No changes to the output on this push; exiting."
37 git commit -m "Automatic deploy to GitHub Pages: ${SHA}"
39 git push "$SSH_REPO" "$TARGET_BRANCH"