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