1# Update the API documentation whenever the `main` branch changes. 2# This documentation lives in its own `docs` branch. 3name: docs 4 5on: 6 push: 7 branches: 8 - 'main' 9 10jobs: 11 update-docs-branch: 12 runs-on: ubuntu-20.04 # latest 13 permissions: 14 contents: write # allow push 15 steps: 16 - name: Checkout 17 uses: actions/checkout@v3 18 with: 19 submodules: true 20 21 - name: Update docs branch 22 run: | 23 ./make-docs.sh 24 25 - name: Commit 26 run: | 27 git config --local user.email "action@github.com" 28 git config --local user.name "GitHub Action" 29 git add --force docs/ 30 git commit --message="update docs" 31 32 - name: Push to docs branch 33 uses: ad-m/github-push-action@v0.6.0 34 with: 35 github_token: ${{ github.token }} 36 branch: docs 37 # Force push so that `docs` branch always looks like `main`, 38 # but with 1 additional "update docs" commit. 39 # This seems simpler than trying to cleanly merge `main` into 40 # `docs` each time. 41 force: true 42