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