make wiki sync happy (#4962)

This commit is contained in:
David Holdeman 2023-01-10 18:08:01 -06:00 committed by GitHub
parent d5b00e1187
commit cf82f74611
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 5 additions and 0 deletions

View File

@ -35,6 +35,10 @@ jobs:
run: |
git remote add best-wiki-git https://github.com/rusefi/rusefi.wiki.git
git fetch best-wiki-git
if [ $(git diff best-wiki-git/master | wc -l) -eq 0 ]; then
echo "skip=true" >> $GITHUB_ENV
exit 0
fi
git show --name-only best-wiki-git/master
git config --local user.email "action@github.com"
git config --local user.name "GitHub Action"
@ -51,6 +55,7 @@ jobs:
- name: Push changes to rusefi_documentation technical wiki
uses: ad-m/github-push-action@master
if: ${{ env.skip != 'true' }}
with:
repository: rusefi/rusefi_documentation
github_token: ${{ secrets.ACCESS_TOKEN }}