release.yml

# This is an action that builds the document and deploys the build document
# to its associated GitHub pages site.

name: release

on:
  push:
    tags:
      - 'v*.*.*'

jobs:
  build:
    runs-on: ubuntu-latest
    steps:
    - uses: actions/checkout@v2
      with:
        fetch-depth: 0
    ############################################################
    - name: Prepare to build the document.
      shell: bash
      run: tools/build/prebuild
    ############################################################
    - name: Collect git metadata
      id: git_metadata
      run: |
        echo ::set-output name=VERSION::${GITHUB_REF#refs/tags/v}
    # The following builds the document in multiple formats for deployment.
    - name: Build the document.
      shell: bash
      run: |
        tools/build/build \
          -d ${{runner.temp}}/output \
          -v ${{ steps.git_metadata.outputs.VERSION }}
    - name: Deploy generated content to gh-pages
      uses: peaceiris/actions-gh-pages@v3
      with:
        github_token: ${{ secrets.GITHUB_TOKEN }}
        publish_dir: ${{runner.temp}}/output
        keep_files: true