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