about summary refs log tree commit diff
diff options
context:
space:
mode:
authorflip1995 <hello@philkrones.com>2020-01-22 21:00:31 +0100
committerflip1995 <hello@philkrones.com>2020-02-12 09:34:26 +0100
commit893e261a99f74b3b925ab66ccfef45acb8b2d82b (patch)
treea89b281d1b5b23fe2a933750d7d4eabf95ebc730
parent92811675ce14d717d04d5d9e8dd89172cbcb0b57 (diff)
downloadrust-893e261a99f74b3b925ab66ccfef45acb8b2d82b.tar.gz
rust-893e261a99f74b3b925ab66ccfef45acb8b2d82b.zip
Add deployment to GHA
-rw-r--r--.github/workflows/deploy.yml72
1 files changed, 72 insertions, 0 deletions
diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml
new file mode 100644
index 00000000000..100adbadd5a
--- /dev/null
+++ b/.github/workflows/deploy.yml
@@ -0,0 +1,72 @@
+name: Deploy
+
+on:
+  push:
+    branches: master
+  release:
+    types: [created]
+
+env:
+  TARGET_BRANCH: 'gh-pages'
+  SHA: '${{ github.sha }}'
+  SSH_REPO: 'git@github.com:${{ github.repository }}.git'
+  TAG_NAME: '${{ github.event.release.GITHUB_REF }}'
+
+jobs:
+  deploy:
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v2.0.0
+    - name: Checkout
+      uses: actions/checkout@v2.0.0
+      with:
+        ref: ${{ env.TARGET_BRANCH }}
+        path: 'out'
+    - name: Deploy
+      run: |
+        set -ex
+
+        echo "Removing the current docs for master"
+        rm -rf out/master/ || exit 0
+
+        echo "Making the docs for master"
+        mkdir out/master/
+        cp util/gh-pages/index.html out/master
+        python ./util/export.py out/master/lints.json
+
+        if [[ -n $TAG_NAME ]]; then
+          echo "Save the doc for the current tag ($TAG_NAME) and point current/ to it"
+          cp -r out/master "out/$TAG_NAME"
+          rm -f out/current
+          ln -s "$TAG_NAME" out/current
+        fi
+
+        # Generate version index that is shown as root index page
+        cp util/gh-pages/versions.html out/index.html
+
+        cd out
+        cat <<-EOF | python - > versions.json
+        import os, json
+        print json.dumps([
+            dir for dir in os.listdir(".") if not dir.startswith(".") and os.path.isdir(dir)
+        ])
+        EOF
+
+        # Now let's go have some fun with the cloned repo
+        git config user.name "GHA CI"
+        git config user.email "gha@ci.invalid"
+
+        if git diff --exit-code --quiet; then
+            echo "No changes to the output on this push; exiting."
+            exit 0
+        fi
+
+        git add .
+        git commit -m "Automatic deploy to GitHub Pages: ${SHA}"
+
+        eval "$(ssh-agent -s)"
+        ssh-add - <<< "${{ secrets.DEPLOY_KEY }}"
+
+        git push "$SSH_REPO" "$TARGET_BRANCH"