Refresh repository list #3
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Refresh repository list | |
| on: | |
| schedule: | |
| # Mondays at 05:17 UTC — off the hour to avoid the top-of-hour scheduling queue | |
| - cron: '17 5 * * 1' | |
| workflow_dispatch: | |
| permissions: | |
| contents: read | |
| # never let two refreshes race to push the same file | |
| concurrency: | |
| group: refresh-repos | |
| cancel-in-progress: false | |
| jobs: | |
| refresh: | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: write | |
| # needed to dispatch the Pages deploy below | |
| actions: write | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - name: Set up mise | |
| uses: jdx/mise-action@9e7f7633ff6f6d6048a9418a68d48f288f50eb14 # v4.2.3 | |
| with: | |
| install: true | |
| cache: true | |
| - name: Regenerate docs/src/data/repos.json | |
| env: | |
| # only used to read public repository metadata from the org | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: mise run docs-repos | |
| - name: Commit and push any changes | |
| id: commit | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: | | |
| if git diff --quiet -- docs/src/data/repos.json; then | |
| echo "No changes to the repository list." | |
| echo "changed=false" >> "$GITHUB_OUTPUT" | |
| exit 0 | |
| fi | |
| git config user.name 'github-actions[bot]' | |
| git config user.email '41898282+github-actions[bot]@users.noreply.github.com' | |
| git add docs/src/data/repos.json | |
| git commit -m 'Refresh the list of public repositories' | |
| git push "https://x-access-token:${GH_TOKEN}@github.com/${GITHUB_REPOSITORY}.git" \ | |
| "HEAD:${GITHUB_REF_NAME}" | |
| echo "changed=true" >> "$GITHUB_OUTPUT" | |
| # A push made with GITHUB_TOKEN does not trigger other workflows, so ask | |
| # for the Pages deploy explicitly. workflow_dispatch is one of the two | |
| # events that GITHUB_TOKEN is allowed to fire. | |
| - name: Trigger the Pages deploy | |
| if: steps.commit.outputs.changed == 'true' | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: gh workflow run deploy.yml --ref "${GITHUB_REF_NAME}" |