deploy-docs.yaml

name: Deploy Docs

on:
  push:
    branches:
      - stable
      - master

# Builds all docs for both stable and master branches.
# In the gh-pages branch, we place:
# stable user-guide at /
# master user-guide at /devel
# master dev-guide at /dev-guide

jobs:
  doc:
    name: Documentation
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
        with:
          fetch-depth: 0
      - name: Install mdbook
        run: |
          mkdir mdbook
          curl -Lf https://github.com/rust-lang/mdBook/releases/download/v0.4.37/mdbook-v0.4.37-x86_64-unknown-linux-gnu.tar.gz | tar -xz --directory=./mdbook
          echo "`pwd`/mdbook" >> $GITHUB_PATH
      - name: Build book
        run: |
          # Build for stable
          git checkout stable
          # Support both old and new directory structure during the transition
          cd doc/user-guide || cd doc
          mdbook build
          mv book ${{ runner.temp }}
          # Build for master
          cd $(git rev-parse --show-toplevel)
          git checkout master
          cd doc/user-guide
          mdbook build
          mv book ${{ runner.temp }}/book/devel
          # Build dev-guide for master
          cd ../dev-guide
          mdbook build
          mv book ${{ runner.temp }}/book/dev-guide
      - name: Deploy to GitHub
        run: |
          cd ${{ runner.temp }}/book
          git init
          git config user.name "Deploy from CI"
          git config user.email ""
          git add . .nojekyll
          git commit -m "Deploy $GITHUB_REF $GITHUB_SHA to gh-pages"
          git remote add origin https://x-access-token:${{ secrets.GITHUB_TOKEN }}@github.com/$GITHUB_REPOSITORY
          git push --force --set-upstream origin master:gh-pages