Skip to content

Commit ca8bb13

Browse files
benjefferybenjeffery
authored
Merge pull request #1054 from benjeffery/disable-docs
Disable doc upload
2 parents b7437eb + 62da951 commit ca8bb13

File tree

1 file changed

+75
-75
lines changed

1 file changed

+75
-75
lines changed

‎.github/workflows/docs.yml‎

Lines changed: 75 additions & 75 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
name: Build Docs
22

33
on:
4-
pull_request_target:
4+
pull_request:
55
push:
66
branches: [main]
77
tags:
@@ -62,77 +62,77 @@ jobs:
6262
- name: Build Docs
6363
run: venv/bin/activate && make -C docs
6464

65-
- name: Wait for others to finish
66-
uses: softprops/turnstyle@v1
67-
with:
68-
same-branch-only: false
69-
env:
70-
GITHUB_TOKEN: ${{ secrets.ADMINBOT_TOKEN }}
71-
72-
- name: Checkout docs site
73-
if: github.repository_owner == env.OWNER
74-
uses: actions/checkout@v2
75-
with:
76-
repository: ${{ env.OWNER }}/${{ env.REPO }}-docs
77-
token: ${{ secrets.ADMINBOT_TOKEN }}
78-
path: ${{ env.REPO }}-docs
79-
80-
- name: Check for diff compared to main branch
81-
if: github.repository_owner == env.OWNER && github.event.pull_request
82-
id: diff
83-
#The html contains commit hashes which we don't want to count as a change
84-
run: |
85-
diff -x .buildinfo -r ${{ env.REPO }}-docs/main docs/_build/html | grep "^[<>]" | grep -v "<title>\|VERSION:" | grep -Ev "\.(css|js)\?" | grep -v "Search\.setIndex" | grep . && echo "::set-output name=change_detected::true" || echo "NO CHANGES"
86-
87-
- name: Copy our docs to the PR specific location
88-
if: github.repository_owner == env.OWNER && github.event.pull_request && steps.diff.outputs.change_detected
89-
working-directory: ${{ env.REPO }}-docs
90-
run: |
91-
rm -rf ${{ github.event.pull_request.number }}
92-
cp -r ../docs/_build/html PR-${{ github.event.pull_request.number }}
93-
94-
- name: Copy our docs to the tag specific location
95-
if: github.repository_owner == env.OWNER && !github.event.pull_request
96-
working-directory: ${{ env.REPO }}-docs
97-
run: |
98-
export DEST=`echo ${GITHUB_REF} | sed -e "s/refs\/heads\///g" | sed -e "s/refs\/tags\///g"`
99-
rm -rf $DEST
100-
cp -r ../docs/_build/html $DEST
101-
102-
- name: Delete closed PRs
103-
if: github.repository_owner == env.OWNER
104-
shell: python
105-
working-directory: ${{ env.REPO }}-docs
106-
run : |
107-
from github import Github
108-
import os
109-
import shutil
110-
g = Github()
111-
repo = g.get_repo("${{ env.OWNER }}/${{ env.REPO }}")
112-
open_prs = [f"PR-{pr.number}" for pr in repo.get_pulls(state="open")]
113-
for name in os.listdir("."):
114-
if name.startswith('PR') and name not in open_prs:
115-
print("Delete:", name)
116-
shutil.rmtree(name)
117-
else:
118-
print("Keep:", name)
119-
120-
121-
- name: Commit --amend docs
122-
if: github.repository_owner == env.OWNER && (steps.diff.outputs.change_detected || (!github.event.pull_request))
123-
working-directory: ${{ env.REPO }}-docs
124-
run: |
125-
git config user.name AdminBOT
126-
git config user.email $COMMIT_EMAIL
127-
git add .
128-
git diff-index --quiet HEAD || git commit --amend --no-edit
129-
git push -f origin main
130-
131-
- name: Comment on PR
132-
if: github.repository_owner == env.OWNER && github.event.pull_request && steps.diff.outputs.change_detected
133-
uses: mshick/add-pr-comment@v1
134-
with:
135-
message: |
136-
📖 Docs for this PR can be previewed [here](https://${{ env.OWNER }}.github.io/${{ env.REPO }}-docs/PR-${{ github.event.pull_request.number }}/)
137-
allow-repeats: false
138-
repo-token: ${{ secrets.ADMINBOT_TOKEN }}
65+
# - name: Wait for others to finish
66+
# uses: softprops/turnstyle@v1
67+
# with:
68+
# same-branch-only: false
69+
# env:
70+
# GITHUB_TOKEN: ${{ secrets.ADMINBOT_TOKEN }}
71+
#
72+
# - name: Checkout docs site
73+
# if: github.repository_owner == env.OWNER
74+
# uses: actions/checkout@v2
75+
# with:
76+
# repository: ${{ env.OWNER }}/${{ env.REPO }}-docs
77+
# token: ${{ secrets.ADMINBOT_TOKEN }}
78+
# path: ${{ env.REPO }}-docs
79+
#
80+
# - name: Check for diff compared to main branch
81+
# if: github.repository_owner == env.OWNER && github.event.pull_request
82+
# id: diff
83+
# #The html contains commit hashes which we don't want to count as a change
84+
# run: |
85+
# diff -x .buildinfo -r ${{ env.REPO }}-docs/main docs/_build/html | grep "^[<>]" | grep -v "<title>\|VERSION:" | grep -Ev "\.(css|js)\?" | grep -v "Search\.setIndex" | grep . && echo "::set-output name=change_detected::true" || echo "NO CHANGES"
86+
#
87+
# - name: Copy our docs to the PR specific location
88+
# if: github.repository_owner == env.OWNER && github.event.pull_request && steps.diff.outputs.change_detected
89+
# working-directory: ${{ env.REPO }}-docs
90+
# run: |
91+
# rm -rf ${{ github.event.pull_request.number }}
92+
# cp -r ../docs/_build/html PR-${{ github.event.pull_request.number }}
93+
#
94+
# - name: Copy our docs to the tag specific location
95+
# if: github.repository_owner == env.OWNER && !github.event.pull_request
96+
# working-directory: ${{ env.REPO }}-docs
97+
# run: |
98+
# export DEST=`echo ${GITHUB_REF} | sed -e "s/refs\/heads\///g" | sed -e "s/refs\/tags\///g"`
99+
# rm -rf $DEST
100+
# cp -r ../docs/_build/html $DEST
101+
#
102+
# - name: Delete closed PRs
103+
# if: github.repository_owner == env.OWNER
104+
# shell: python
105+
# working-directory: ${{ env.REPO }}-docs
106+
# run : |
107+
# from github import Github
108+
# import os
109+
# import shutil
110+
# g = Github()
111+
# repo = g.get_repo("${{ env.OWNER }}/${{ env.REPO }}")
112+
# open_prs = [f"PR-{pr.number}" for pr in repo.get_pulls(state="open")]
113+
# for name in os.listdir("."):
114+
# if name.startswith('PR') and name not in open_prs:
115+
# print("Delete:", name)
116+
# shutil.rmtree(name)
117+
# else:
118+
# print("Keep:", name)
119+
#
120+
#
121+
# - name: Commit --amend docs
122+
# if: github.repository_owner == env.OWNER && (steps.diff.outputs.change_detected || (!github.event.pull_request))
123+
# working-directory: ${{ env.REPO }}-docs
124+
# run: |
125+
# git config user.name AdminBOT
126+
# git config user.email $COMMIT_EMAIL
127+
# git add .
128+
# git diff-index --quiet HEAD || git commit --amend --no-edit
129+
# git push -f origin main
130+
#
131+
# - name: Comment on PR
132+
# if: github.repository_owner == env.OWNER && github.event.pull_request && steps.diff.outputs.change_detected
133+
# uses: mshick/add-pr-comment@v1
134+
# with:
135+
# message: |
136+
# 📖 Docs for this PR can be previewed [here](https://${{ env.OWNER }}.github.io/${{ env.REPO }}-docs/PR-${{ github.event.pull_request.number }}/)
137+
# allow-repeats: false
138+
# repo-token: ${{ secrets.ADMINBOT_TOKEN }}

0 commit comments

Comments
 (0)