This repository was archived by the owner on Mar 13, 2024. It is now read-only.
File tree Expand file tree Collapse file tree 4 files changed +52
-4
lines changed
Expand file tree Collapse file tree 4 files changed +52
-4
lines changed Original file line number Diff line number Diff line change 1010jobs :
1111 lint :
1212 # pull requests are a duplicate of a branch push if within the same repo.
13- if : github.event_name != 'pull_request' || github.event.pull_request.repository = = github.repository
13+ if : github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name ! = github.repository
1414 runs-on : ubuntu-latest
1515
1616 steps :
2929 tox -e pre-commit,mypy
3030
3131 test :
32- if : github.event_name != 'pull_request' || github.event.pull_request.repository = = github.repository
32+ if : github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name ! = github.repository
3333 strategy :
3434 fail-fast : false
3535 matrix :
7070 files : cov.xml
7171
7272 container :
73- if : github.event_name != 'pull_request' || github.event.pull_request.repository = = github.repository
73+ if : github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name ! = github.repository
7474 runs-on : ubuntu-latest
7575 permissions :
7676 contents : read
Original file line number Diff line number Diff line change 66
77jobs :
88 docs :
9+ if : github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name != github.repository
910 strategy :
1011 fail-fast : false
1112 matrix :
1415 runs-on : ubuntu-latest
1516
1617 steps :
18+ - name : Dump github context
19+ run : echo "$GITHUB_CONTEXT"
20+ shell : bash
21+ env :
22+ GITHUB_CONTEXT : ${{ toJson(github) }}
23+
1724 - name : Avoid git conflicts when tag and branch pushed at same time
1825 if : startsWith(github.ref, 'refs/tags')
1926 run : sleep 60
Original file line number Diff line number Diff line change 1+ name : Docs Cleanup CI
2+
3+ # delete branch documentation when a branch is deleted
4+ # also allow manually deleting a documentation version
5+ on :
6+ delete :
7+ workflow_dispatch :
8+ inputs :
9+ version :
10+ description : " documentation version to DELETE"
11+ required : true
12+ type : string
13+
14+ jobs :
15+ remove :
16+ if : github.event.ref_type == 'branch' || github.event_name == 'workflow_dispatch'
17+ runs-on : ubuntu-latest
18+
19+ steps :
20+ - name : checkout
21+ uses : actions/checkout@v2
22+ with :
23+ ref : gh-pages
24+
25+ - name : removing documentation for branch ${{ github.event.ref }}
26+ if : ${{ github.event_name != 'workflow_dispatch' }}
27+ run : echo "remove_me=${{ github.event.ref }}" >> $GITHUB_ENV
28+
29+ - name : manually removing documentation version ${{ github.event.inputs.version }}
30+ if : ${{ github.event_name == 'workflow_dispatch' }}
31+ run : echo "remove_me=${{ github.event.inputs.version }}" >> $GITHUB_ENV
32+
33+ - name : update index and push changes
34+ run : |
35+ echo removing redundant documentation version ${{ env.remove_me }}
36+ rm -r ${{ env.remove_me }}
37+ sed -i /${{ env.remove_me }}/d versions.txt
38+ git config --global user.name 'GitHub Actions Docs Cleanup CI'
39+ git config --global user.email '[email protected] ' 40+ git commit -am"removing redundant docs version ${{ env.remove_me }}"
41+ git push
Original file line number Diff line number Diff line change @@ -12,4 +12,4 @@ Explanation of how the library works and why it works that way.
1212 explanations/why-src
1313 explanations/why-pre-commit
1414 explanations/features
15- explanations/decisions
15+ explanations/decisions
You can’t perform that action at this time.
0 commit comments