2019-11-14 20:30:35 +00:00
|
|
|
# The objective of this GitHub Action is to update the DIRECTORY.md file (if needed)
|
|
|
|
# when doing a git push
|
2019-11-14 19:27:31 +00:00
|
|
|
name: directory_writer
|
2019-11-14 20:30:35 +00:00
|
|
|
on: [push]
|
2019-11-14 19:27:31 +00:00
|
|
|
jobs:
|
|
|
|
build:
|
|
|
|
runs-on: ubuntu-latest
|
2019-11-14 20:30:35 +00:00
|
|
|
steps:
|
2022-07-07 03:25:25 +00:00
|
|
|
- uses: actions/checkout@v1 # v1, NOT v2 or v3
|
|
|
|
- uses: actions/setup-python@v4
|
|
|
|
with:
|
|
|
|
python-version: 3.x
|
2020-03-14 05:37:44 +00:00
|
|
|
- name: Write DIRECTORY.md
|
2019-11-14 19:27:31 +00:00
|
|
|
run: |
|
|
|
|
scripts/build_directory_md.py 2>&1 | tee DIRECTORY.md
|
2020-03-14 06:33:14 +00:00
|
|
|
git config --global user.name github-actions
|
|
|
|
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
|
2020-03-14 05:37:44 +00:00
|
|
|
run: |
|
2020-03-14 06:33:14 +00:00
|
|
|
git add DIRECTORY.md
|
|
|
|
git commit -am "updating DIRECTORY.md" || true
|
2020-05-16 06:49:56 +00:00
|
|
|
git push --force origin HEAD:$GITHUB_REF || true
|