File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 11name : Doc Cleanup
22on :
3- push :
4- branches :
5- - gh-pages
3+ # runs on the 1st day of every month at 03:00 UTC
4+ schedule :
5+ - cron : ' 0 3 1 * * '
66 workflow_dispatch :
7+ permissions :
8+ contents : write
79jobs :
810 doc-cleanup :
911 runs-on : ubuntu-latest
1012 steps :
1113 - name : Checkout gh-pages branch
12- uses : actions/checkout@v4
14+ uses : actions/checkout@v7
1315 with :
1416 ref : gh-pages
1517 - name : Delete old docs
1618 run : |
17- keep=$(readlink stable)
19+ keep=" $(readlink stable)"
1820 git config user.name "Documenter.jl"
1921 git config user.email "documenter@juliadocs.github.io"
20- git rm -rf v[0-9]*.[0-9]* && git checkout HEAD -- $keep
21- if git commit -m "keep latest docs only" ; then
22+ git rm -rf --ignore-unmatch "v[0-9]*.[0-9]*" "previews/*"
23+ git checkout HEAD -- "$keep"
24+ if git diff --cached --quiet; then
25+ echo "No old docs or previews to delete"
26+ else
27+ git commit -m "Delete old docs and previews"
2228 git branch gh-pages-new $(echo "delete history" | git commit-tree HEAD^{tree})
2329 git push --force origin gh-pages-new:gh-pages
2430 fi
You can’t perform that action at this time.
0 commit comments