Add CI script to create docs on new releases

.github/workflows/create-release-docs.yml

@@ -0,0 +1,54 @@
+name: "Create release docs"
+on:
+  release:
+    types:
+      - created
+
+jobs:
+  build:
+    runs-on: ubuntu-18.04
+    steps:
+      - name: Checkout rgbds@master
+        uses: actions/checkout@v2
+        with:
+          repository: gbdev/rgbds
+          ref: master
+          path: rgbds
+      - name: Checkout rgbds-www@master
+        uses: actions/checkout@v2
+        with:
+          repository: gbdev/rgbds-www
+          ref: master
+          path: rgbds-www
+      - name: Build and install mandoc
+        run: |
+          sudo apt-get -qq update
+          sudo apt-get install -yq zlib1g-dev
+          wget 'http://mandoc.bsd.lv/snapshots/mandoc-1.14.5.tar.gz'
+          tar xf mandoc-1.14.5.tar.gz
+          cd mandoc-1.14.5
+          ./configure
+          make
+          sudo make install
+      - name: Update pages
+        working-directory: rgbds
+        run: |
+          ./.github/actions/get-pages.sh ../rgbds-www/_documentation ${GITHUB_REF}
+      - name: Push new pages
+        working-directory: rgbds-www
+        run: |
+          mkdir -p -m 700 ~/.ssh
+          echo "${{ secrets.SSH_KEY_SECRET }}" > ~/.ssh/id_ed25519
+          chmod 0600 ~/.ssh/id_ed25519
+          eval $(ssh-agent -s)
+          ssh-add ~/.ssh/id_ed25519
+          git config --global user.name "GitHub Action"
+          git config --global user.email "community@gbdev.io"
+          git add .
+          git commit -m "Create RGBDS ${GITHUB_REF} documentation"
+          if git remote | grep -q origin; then
+            git remote set-url origin git@github.com:gbdev/rgbds-www.git
+          else
+            git remote add origin git@github.com:gbdev/rgbds-www.git
+          fi
+          git push origin master