File tree Expand file tree Collapse file tree 1 file changed +9
-6
lines changed Expand file tree Collapse file tree 1 file changed +9
-6
lines changed Original file line number Diff line number Diff line change 2525 ref : gh-pages
2626 - name : Delete preview and history + push changes
2727 run : |
28- git config user.name "Documenter.jl"
29- git config user.email "[email protected] " 30- git rm -rf previews/*
31- git commit -m "delete previews directory"
32- git branch gh-pages-new $(echo "delete history" | git commit-tree HEAD^{tree})
33- git push --force origin gh-pages-new:gh-pages
28+ preview_directory=previews/PR${{ github.event.number }}
29+ if [[ -d "${preview_directory}" ]]; then
30+ git config user.name "${{github.actor}}"
31+ git config user.email "${{github.actor_id}}+${{github.actor}}@users.noreply.github.com"
32+ git rm -rf "${preview_directory}"
33+ git commit -m 'Cleanup docs for PR #${{ github.event.number }}'
34+ git branch gh-pages-new $(echo "Delete history" | git commit-tree HEAD^{tree})
35+ git push --force origin gh-pages-new:gh-pages
36+ fi
You can’t perform that action at this time.
0 commit comments