# The objective of this GitHub Action is to update the DIRECTORY.md file (if needed) # when doing a git push name: directory_writer on: [push] jobs: build: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 with: fetch-depth: 0 - uses: actions/setup-python@v5 with: python-version: 3.x - name: Write DIRECTORY.md run: | scripts/build_directory_md.py 2>&1 | tee DIRECTORY.md git config --global user.name "$GITHUB_ACTOR" git config --global user.email "$GITHUB_ACTOR@users.noreply.github.com" git remote set-url origin https://x-access-token:${{ secrets.GITHUB_TOKEN }}@github.com/$GITHUB_REPOSITORY - name: Update DIRECTORY.md run: | git add DIRECTORY.md git commit -am "updating DIRECTORY.md" || true git push --force origin HEAD:$GITHUB_REF || true