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:
|
2019-12-26 11:50:12 +00:00
|
|
|
- uses: actions/checkout@v2
|
2019-11-15 02:22:23 +00:00
|
|
|
- uses: actions/setup-python@v1
|
2019-11-14 19:27:31 +00:00
|
|
|
with:
|
2019-11-15 02:22:23 +00:00
|
|
|
python-version: 3.x
|
2019-11-14 19:27:31 +00:00
|
|
|
- name: Update DIRECTORY.md
|
|
|
|
run: |
|
|
|
|
scripts/build_directory_md.py 2>&1 | tee DIRECTORY.md
|
2019-11-14 20:30:35 +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
|
2020-01-10 01:08:49 +00:00
|
|
|
git add DIRECTORY.md
|
2019-11-15 02:22:23 +00:00
|
|
|
git commit -am "updating DIRECTORY.md" || true
|
|
|
|
git push --force origin HEAD:$GITHUB_REF || true
|