.github/workflows/docs.yml


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34

name: docs
on:
  pull_request:
    types: [opened, synchronize, reopened, ready_for_review]

permissions: {}

jobs:
  docs:
    runs-on: ubuntu-latest
    if: github.event.pull_request.draft == false
    permissions:
      contents: write
      pull-requests: write
    steps:
      - uses: actions/checkout@v6
        with:
          persist-credentials: false
      - uses: ./.github/actions/setup

      - name: Generate docs
        run: |
          make doc
          if [ -n "$(git status --porcelain)" ]; then
            echo "::error::Job failed, run 'make doc' and commit your doc changes."
            echo "::error::The doc generation produces the following changes:"
            git diff --color --exit-code
          fi

      - name: lintdoc
        run: make lintdoc

      - name: linterrcodes
        run: make linterrcodes