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