shithub: rgbds

ref: d8e8b796e7aa15956f1e648edbdc9ab6f7edb555
dir: /.github/workflows/create-release-docs.yml/

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