# Cherry-pick documentation commits from main onto dev. # Non-doc files on main (relative to dev) fail the job. name: Sync docs on: push: branches: [main] paths: - README.md - Readme.md - Readme.en.md - Doxyfile - docs/** permissions: contents: write pull-requests: write jobs: sync: name: sync-docs runs-on: ubuntu-latest timeout-minutes: 15 steps: - name: Checkout timeout-minutes: 10 uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: fetch-depth: 0 token: ${{ secrets.GITHUB_TOKEN }} - name: Sync documentation to dev timeout-minutes: 10 env: GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} CI: "true" run: | set -euo pipefail git config user.name "github-actions[bot]" git config user.email "41898282+github-actions[bot]@users.noreply.github.com" python3 scripts/release.py sync-docs