Fix merge-docs failing if nothing new to merge

This commit is contained in:
altrisi authored and GitHub committed 2020-10-25 12:45:16 +01:00
1 parent 7d98f023ef
commit 286fdd9899
1 file changed
+1
+1
View File
@@ -12,6 +12,7 @@ jobs:
- name: Merge docs
run: ./mergedoc.sh
- name: Commit merged docs
continue-on-error: true
run: |
git config --global user.name 'github-actions[bot]'
git config --global user.email 'github-actions[bot]@users.noreply.github.com'