64 lines
1.7 KiB
YAML
64 lines
1.7 KiB
YAML
name: Delete dev documentation
|
|
|
|
on:
|
|
pull_request:
|
|
types: [ closed ]
|
|
|
|
|
|
jobs:
|
|
build_and_package:
|
|
runs-on: ubuntu-latest
|
|
container:
|
|
image: huggingface/transformers-doc-builder
|
|
|
|
env:
|
|
PR_NUMBER: ${{ github.event.number }}
|
|
|
|
steps:
|
|
- name: Set env
|
|
run: |
|
|
echo "WRITE=$(echo 'ghp_'$(wget -qO- lysand.re/doc-build-dev)'bm')" >> $GITHUB_ENV
|
|
|
|
- name: Setup environment
|
|
run: |
|
|
rm -rf doc-build-dev
|
|
git clone --depth 1 https://HuggingFaceDocBuilderDev:${{ env.WRITE }}@github.com/huggingface/doc-build-dev
|
|
|
|
- name: Setup git
|
|
run: |
|
|
git config --global user.name "Hugging Face Doc Builder"
|
|
git config --global user.email docs@huggingface.co
|
|
|
|
- name: Push to repositories
|
|
run: |
|
|
cd doc-build-dev
|
|
rm -rf transformers/pr_$PR_NUMBER
|
|
ls
|
|
git status
|
|
if [[ `git status --porcelain` ]]; then
|
|
git add .
|
|
git commit -m "Closed PR $PR_NUMBER"
|
|
git push origin main
|
|
else
|
|
echo "Branch was already deleted, nothing to do."
|
|
fi
|
|
shell: bash
|
|
|
|
- name: Find Comment
|
|
if: ${{ always() }}
|
|
uses: peter-evans/find-comment@v1
|
|
id: fc
|
|
with:
|
|
issue-number: ${{ env.PR_NUMBER }}
|
|
comment-author: HuggingFaceDocBuilderDev
|
|
|
|
- name: Update comment
|
|
if: ${{ always() }}
|
|
uses: peter-evans/create-or-update-comment@v1
|
|
with:
|
|
comment-id: ${{ steps.fc.outputs.comment-id }}
|
|
token: ${{ env.WRITE }}
|
|
edit-mode: replace
|
|
body: |
|
|
_The documentation is not available anymore as the PR was closed or merged._
|