@@ -3,6 +3,8 @@ name: Doc Preview Cleanup
33on :
44 pull_request :
55 types : [closed]
6+ schedule :
7+ - cron : " 0 0 */14 * *"
68
79jobs :
810 doc-preview-cleanup :
@@ -13,16 +15,65 @@ jobs:
1315 with :
1416 ref : gh-pages
1517
16- - name : Delete preview and history
18+ - uses : julia-actions/setup-julia@v2
19+ with :
20+ version : ' 1'
21+ - uses : julia-actions/cache@v2
22+
23+ - name : Check for stale PR previews
24+ shell : julia {0}
1725 run : |
18- git config user.name "Documenter.jl"
19- git config user.email "documenter@juliadocs.github.io"
20- git rm -rf "previews/PR$PRNUM"
21- git commit -m "delete preview"
22- git branch gh-pages-new $(echo "delete history" | git commit-tree HEAD^{tree})
23- env :
24- PRNUM : ${{ github.event.number }}
26+ using Pkg
27+ Pkg.activate(temp = true)
28+ Pkg.add(["HTTP", "JSON3"])
29+
30+ using HTTP
31+ using JSON3
32+ using Dates
33+
34+ repo = ENV["GITHUB_REPOSITORY"]
35+ retention_days = 14
36+
37+ pr_previews = map(filter(startswith("PR"), readdir("previews"))) do dir
38+ parse(Int, match(r"PR(\d*)", dir)[1])
39+ end
40+
41+ function all_prs()
42+ url = "https://api.github.com/repos/$repo/pulls?per_page=100;page=$(page)"
43+ query_prs(page) = JSON3.read(HTTP.get(url).body)
44+ prs = []
45+ page = 1
46+ while true
47+ page_prs = query_prs(page)
48+ isempty(page_prs) && break
49+ append!(prs, page_prs)
50+ page += 1
51+ end
52+ return prs
53+ end
54+ prs = all_prs()
55+ open_within_threshold = map(x -> x.number, filter(prs) do pr
56+ time = DateTime(pr.updated_at[1:19], ISODateTimeFormat)
57+ return pr.state == "open" && Dates.days(now() - time) <= retention_days
58+ end)
59+
60+ stale_previews = setdiff(pr_previews, open_within_threshold)
61+ @info "Found $(length(stale_previews)) stale previews"
62+
63+ if isempty(stale_previews)
64+ @info "No stale previews"
65+ exit(1)
66+ end
2567
68+ for pr in stale_previews
69+ path = joinpath("previews", "PR$pr")
70+ @info "Removing $path"
71+ run(`git rm -rf $path`)
72+ end
2673 - name : Push changes
2774 run : |
28- git push --force origin gh-pages-new:gh-pages
75+ git config user.name "Documenter.jl"
76+ git config user.email "documenter@juliadocs.github.io"
77+ git commit -m "delete preview"
78+ git branch gh-pages-new $(echo "delete history" | git commit-tree HEAD^{tree})
79+ git push --force origin gh-pages-new:gh-pages
0 commit comments