docs.yml

name: Documentation

on:
  push:
    branches: [master]
    tags: ["*"]
  pull_request:
    # Check all PR

jobs:
  build-and-publish:
    runs-on: ubuntu-24.04
    steps:
      - uses: actions/checkout@v4
      - name: setup Julia
        uses: julia-actions/setup-julia@v2
        with:
          version: lts
      - name: build documentation
        run: |
          julia -e 'using Pkg; Pkg.add("Documenter")'
          julia docs/make.jl
      - name: put documentation in the website
        run: |
          git clone https://github.com/$GITHUB_REPOSITORY --branch gh-pages gh-pages
          rm -rf gh-pages/.git

          REF_KIND=$(echo $GITHUB_REF | cut -d / -f2)
          if [[ "$REF_KIND" == "tags" ]]; then
              TAG=${GITHUB_REF#refs/tags/}
              mv docs/build/ gh-pages/$TAG
          else
              rm -rf gh-pages/latest
              mv docs/build/ gh-pages/latest
          fi
      - name: deploy to gh-pages
        if: github.event_name == 'push'
        uses: peaceiris/actions-gh-pages@v4
        with:
          github_token: ${{ secrets.GITHUB_TOKEN }}
          publish_dir: ./gh-pages/
          force_orphan: true