123456789101112131415161718192021222324252627 |
- name: docs
- on:
- pull_request:
- types: [opened, synchronize, reopened, ready_for_review]
- jobs:
- docs:
- runs-on: ubuntu-latest
- if: github.event.pull_request.draft == false
- permissions:
- contents: write
- pull-requests: write
- steps:
- - uses: actions/checkout@v4
- - 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: Validate docs
- run: make lintdoc
|