File tree Expand file tree Collapse file tree 1 file changed +5
-7
lines changed Expand file tree Collapse file tree 1 file changed +5
-7
lines changed Original file line number Diff line number Diff line change @@ -124,13 +124,11 @@ jobs:
124
124
git checkout Production
125
125
git config --local user.email "atomvm-doc-bot@users.noreply.github.com"
126
126
git config --local user.name "AtomVM Doc Bot"
127
- if [ -n "$(git status --porcelain=v1)" ]; then
128
- git add .
129
- git commit -m "Update Documentation"
130
- echo "PUBLISH=true" >> "$GITHUB_OUTPUT"
131
- fi
127
+ ls -la doc/
128
+ git add .
129
+ git diff --exit-code || git commit -m "Update Documentation"
132
130
- name : Push changes
133
- if : github.repository == 'atomvm/AtomVM' && steps.commit_files.outputs.PUBLISH == 'true'
131
+ if : github.repository == 'atomvm/AtomVM'
134
132
working-directory : /home/runner/work/AtomVM/AtomVM/www
135
133
run : |
136
134
eval `ssh-agent -t 60 -s`
@@ -139,4 +137,4 @@ jobs:
139
137
ssh-keyscan github.com >> ~/.ssh/known_hosts
140
138
git remote add push_dest "git@github.com:atomvm/atomvm_www.git"
141
139
git fetch push_dest
142
- git push --set-upstream push_dest Production
140
+ git diff --exit-code origin/Production || git push --set-upstream push_dest Production
You can’t perform that action at this time.
0 commit comments