Adds a delay after push.

main
tommie 2023-05-12 15:11:21 +02:00 committed by GitHub
parent 1ff2086d5a
commit eb6579c665
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 8 additions and 1 deletions

View File

@ -207,8 +207,15 @@ jobs:
fi
- name: Push changes
uses: ad-m/github-push-action@v0.6.0
uses: ad-m/github-push-action@master
if: github.ref_name == 'main'
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
branch: ${{ github.ref }}
# GitHub shows an inconsistent delay with pulling right after pushing. Since we push
# for multiple distributions, we have to make sure the next checkout doesn't conflict
# with the current.
- name: Delay 30 seconds for pushed changes to be visible
run: sleep 30s
shell: bash