File tree Expand file tree Collapse file tree 1 file changed +33
-0
lines changed Expand file tree Collapse file tree 1 file changed +33
-0
lines changed Original file line number Diff line number Diff line change 1+ name : Doc Preview Cleanup
2+
3+ on :
4+ pull_request :
5+ types : [closed]
6+
7+ # Ensure that only one "Doc Preview Cleanup" workflow is force pushing at a time
8+ concurrency :
9+ group : doc-preview-cleanup
10+ cancel-in-progress : false
11+
12+ jobs :
13+ doc-preview-cleanup :
14+ runs-on : ubuntu-latest
15+ permissions :
16+ contents : write
17+ steps :
18+ - name : Checkout gh-pages branch
19+ uses : actions/checkout@v4
20+ with :
21+ ref : gh-pages
22+ - name : Delete preview and history + push changes
23+ run : |
24+ if [ -d "${preview_dir}" ]; then
25+ git config user.name "Documenter.jl"
26+ git config user.email "[email protected] " 27+ git rm -rf "${preview_dir}"
28+ git commit -m "delete preview"
29+ git branch gh-pages-new $(echo "delete history" | git commit-tree HEAD^{tree})
30+ git push --force origin gh-pages-new:gh-pages
31+ fi
32+ env :
33+ preview_dir : previews/PR${{ github.event.number }}
You can’t perform that action at this time.
0 commit comments